fact: Fixpoint even_ind' (P:nat->Prop)(exp1:P 0) (exp2:forall n:nat, even n -> P n -> P (S (S n)))(n:nat)(t:even n) {struct t} : P n := match t in (even x) return P x with | O_even => exp1 | plus_2_even p t' => exp2 p t' (even_ind' P exp1 exp2 p t') end.
imports: ZArith List Arith Zwf Relations Inverse_Image