Your Theorem T1
is not equivalent to the Obligation
. In the latter, you're supposed to build an element of Nat
, which itself is a Type
(btw, why aren't you using Set
here? You do not seem to be manipulating higher-order types in this development).
As the error message says, you cannot perform a case analysis (inversion
is built upon that) on an element of Prop
for that (see in particular section 4.5.4 of the Coq manual). However, in this case, you're not interested in building an actual Nat
, you merely want to prove that this case is impossible. For that, you can apply False_rect
(or False_rec
if you choose to go with Set
rather than Type
), which will leave you to prove False
. False
being a Prop
, you then can use inversion H1
.
Note that there is a problem in the second branch of your definition of pred
: you cannot use (pred nat2 H1)
, as H1
is not a proof of pos nat2
. The easiest way is probably to leave an hole here also: (pred nat2 _)
, which can be trivially solved with an inversion
(this time, you must build a term of type pos nat2
, i.e. something that lives in Prop
).