proposition: Lemma projectionListInd : forall (n m : nat) (p1 p2 : m <= n), projectionList n m p1 = projectionList n m p2.
proof: Proof. intros; unfold projectionList in |- *. induction m as [| m Hrecm]. - reflexivity. - simpl in |- *. rewrite (Hrecm (le_S_n m n (le_S (S m) n p1)) (le_S_n m n (le_S (S m) n p2))). now rewrite (evalProjFuncInd _ _ (Compat815.lt_S_n m n (Compat815.le_lt_n_Sm (S m) n p1)) (Compat815.lt_S_n m n (Compat815.le_lt_n_Sm (S m) n p2))). Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)