proposition: Lemma projectionListId : forall (n : nat) (f : naryFunc n) (p : n <= n), extEqual n f (evalComposeFunc n n (projectionList n n p) f).
proof: Proof. intros; induction n as [| n Hrecn]. - cbn in |- *; reflexivity. - cbn in |- *; intros; fold (naryFunc n) in |- *. destruct (eq_nat_dec n n) as [a | b]. + apply extEqualTrans with (evalComposeFunc n (S n) (Vector.cons (naryFunc n) (evalConstFunc n c) n (projectionList n n (le_n n))) f). * apply extEqualTrans with (evalComposeFunc n n (projectionList n n (le_n n)) (f c)). -- apply Hrecn. -- clear Hrecn a p; generalize (projectionList n n (le_n n)). generalize f c; clear f c. assert (H: forall (m : nat) (f : naryFunc (S m)) (c : nat) (v : Vector.t (naryFunc n) m), extEqual n (evalComposeFunc n m v (f c)) (evalComposeFunc n (S m) (Vector.cons (naryFunc n) (evalConstFunc n c) m v) f)). ++ intros; induction n as [| n Hrecn]. ** cbn in |- *; reflexivity. ** cbn in |- *; intros; fold (naryFunc n) in |- *. apply Hrecn. ++ apply H. * apply extEqualCompose. -- unfold extEqualVector in |- *. cbn; split. ++ apply extEqualRefl. ++ apply (projectionListApplyParam n n c (le_n n) (le_S_n n (S n) (le_S (S n) (S n) p))). -- apply extEqualRefl. + now destruct b. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)