proposition: Lemma evalPrimRecParam : forall (n c d : nat) (g : naryFunc (S n)) (h : naryFunc (S (S (S n)))), evalPrimRecFunc n (g d) (fun x y : nat => h x y d) c =x= evalPrimRecFunc (S n) g h c d.
proof: Proof. induction c as [| c Hrecc]. - intros; cbn in |- *; apply extEqualRefl. - intros; cbn in |- *; apply extEqualCompose2; auto. apply extEqualRefl. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)