proposition: Lemma evalProjFuncInd : forall (n m : nat) (p1 p2 : m < n), evalProjFunc n m p1 = evalProjFunc n m p2.
proof: Proof. induction n as [| n Hrecn]. - intros; destruct (Nat.nlt_0_r _ p1). - intros; cbn in |- *; destruct (eq_nat_dec m n) as [e|ne]. + reflexivity. + rewrite (Hrecn _ match Compat815.le_lt_or_eq m n (Compat815.lt_n_Sm_le m n p1) with | or_introl l2 => l2 | or_intror l2 => False_ind (m < n) (ne l2) end match Compat815.le_lt_or_eq m n (Compat815.lt_n_Sm_le m n p2) with | or_introl l2 => l2 | or_intror l2 => False_ind (m < n) (ne l2) end); reflexivity. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)