proposition: Lemma evalStrongRecHelp1 : forall (f : naryFunc 2) (n m : nat), m < n -> codeNth (n - m.+1) (evalStrongRecHelp _ f n) = evalStrongRec _ f m.
proof: Proof. assert (H: forall (f : naryFunc 2) (n : nat), evalStrongRecHelp _ f n = codeList (listValues f n)). { intros f n; induction n as [| n Hrecn]. - simpl in |- *; unfold evalStrongRecHelp in |- *; simpl in |- *. reflexivity. - unfold evalStrongRecHelp in |- *; simpl in |- *; unfold evalStrongRecHelp in Hrecn; simpl in Hrecn; rewrite Hrecn. unfold evalStrongRec in |- *; simpl in |- *. now rewrite cPairProjections1, Hrecn. } intros f n m H0; rewrite H, codeNthCorrect. induction n as [| n Hrecn]. - elim (Nat.nlt_0_r _ H0). - induction (Compat815.le_lt_or_eq _ _ H0). rewrite Nat.sub_succ_l; simpl in |- *. rewrite Hrecn. reflexivity. apply Nat.succ_lt_mono; auto. apply Compat815.lt_n_Sm_le; auto. inversion H1. rewrite Nat.sub_diag; reflexivity. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction