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