See my comment above. | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		solomatov on March 25, 2015 \| parent \| context \| favorite \| on: Proving false in Coq using an implementation bug See my comment above.

llcv on March 25, 2015 [–]

Ok. But if you just introduce an symbol with type NatInd, everything works fine?

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact