proposition: Lemma codeAppCorrect (l1 l2 : list nat): codeApp (codeList l1) (codeList l2) = codeList (l1 ++ l2).
proof: Proof. unfold codeApp; set (f := fun n Hrecs p1 : nat => switchPR n (S (cPair (cPairPi1 (pred n)) (codeNth (n - S (cPairPi2 (pred n))) Hrecs))) p1). induction l1 as [| a l1 Hrecl1]. - unfold evalStrongRec; simpl. now rewrite cPairProjections1. - simpl; unfold evalStrongRec; unfold evalComposeFunc. unfold evalOneParamList; rewrite computeEvalStrongRecHelp. unfold f at 2 ; unfold pred. set (n := S (cPair a (codeList l1))) in *; simpl. repeat rewrite cPairProjections1 || rewrite cPairProjections2. replace (codeList (l1 ++ l2)) with (codeNth (cPair a (codeList l1) - codeList l1) (evalStrongRecHelp 1 f n (codeList l2))). + reflexivity. + assert (H: extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 f n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S (codeList l1)) b)) (evalStrongRec 1 f (codeList l1))). { apply (evalStrongRecHelp2 1). unfold n in |- *. apply Compat815.le_lt_n_Sm. apply cPairLe2. } simpl in H; rewrite H; auto. Qed.
imports: hydras.Ackermann(primRec cPair) hydras.Ackermann(ListExt) Coq(Arith) hydras(extEqualNat Compat815)