proposition: Lemma reduce2ndCompose : forall (c n m : nat) (v : Vector.t (naryFunc n) m) (n0 : naryFunc n) (g : naryFunc (S (S m))), extEqual n (evalComposeFunc n _ (Vector.cons (naryFunc n) n0 _ (Vector.cons (naryFunc n) (evalConstFunc n c) _ v)) g) (evalComposeFunc n _ (Vector.cons (naryFunc n) n0 _ v) (fun x : nat => g x c)).
proof: Proof. induction n as [| n Hrecn]. - cbn in |- *; auto. - cbn in |- *; fold (naryFunc n) in |- *; intros; apply Hrecn. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)