proposition: Lemma projectionListApplyParam : forall (m n c : nat) (p1 : m <= n) (p2 : m <= S n), extEqualVector _ _ (projectionList n m p1) (evalOneParamList n m c (projectionList (S n) m p2)).
proof: Proof. unfold extEqualVector, projectionList in |- *. simple induction m. - simpl in |- *; auto. - intros; simpl in |- *. destruct (eq_nat_dec n n0). + elim (Compat815.lt_not_le n (S n)). apply Nat.lt_succ_diag_r . rewrite <- e in p1; auto. + split. rewrite (evalProjFuncInd _ _ (Compat815.lt_S_n n n0 (Compat815.le_lt_n_Sm (S n) n0 p1)) match Compat815.le_lt_or_eq n n0 (Compat815.lt_n_Sm_le n n0 (Compat815.lt_S_n n (S n0) (Compat815.le_lt_n_Sm (S n) (S n0) p2))) with | or_introl l2 => l2 | or_intror l2 => False_ind (n < n0) (n1 l2) end). * apply extEqualRefl. * apply H. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)