error.v

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