error1.v

Error: Abstracting over the term "b" leads to a term
fun b0 : bool =>
(i >? 0) = b0 ->
(if b0 as res0 return (res0 = b0 -> bool)
 then fun H : true = b0 => f (i - 1) (h_obligation_1 i H)
 else fun _ : false = b0 => false) eq_refl = true -> 
(i + 1 >? 0) = true
which is ill-typed.
Reason is: Illegal application: 
The term "h_obligation_1" of type
 "forall i : Z, true = (i >? 0) -> (i - 1 >=? 0) = true"
cannot be applied to the terms
 "i" : "Z"
 "H" : "true = b0"
The 2nd term has type "true = b0" which should be coercible to
 "true = (i >? 0)".