proposition: Lemma reduce1stCompose : forall (c n m : nat) (v : Vector.t (naryFunc n) m) (g : naryFunc (S m)), extEqual n (evalComposeFunc n _ (Vector.cons (naryFunc n) (evalConstFunc n c) _ v) g) (evalComposeFunc n _ v (g 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)