proposition: Lemma extEqualPrimRec : forall (n : nat) (g1 g2 : naryFunc n) (h1 h2 : naryFunc (S (S n))), g1 =x= g2 -> h1 =x= h2 -> (evalPrimRecFunc n g1 h1: naryFunc (S n)) =x= evalPrimRecFunc n g2 h2.
proof: Proof. intros; simpl in |- *; intros. induction c as [| c Hrecc]. - simpl in |- *; auto. - simpl in |- *. cut (extEqual n (evalPrimRecFunc n g1 h1 c) (evalPrimRecFunc n g2 h2 c)). + cut (extEqual (S n) (h1 c) (h2 c)). * generalize (h1 c) (h2 c) (evalPrimRecFunc n g1 h1 c) (evalPrimRecFunc n g2 h2 c). fold (naryFunc (S n)) in |- *. clear Hrecc H0 h1 h2 g1 g2 H. induction n as [| n Hrecn]. -- simpl in |- *; intros; rewrite H0; apply H. -- simpl in |- *; intros; apply Hrecn. ++ simpl in |- *; intros; apply H. ++ apply H0. * simpl in |- *; intros; apply H0. + auto. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)