proposition: Lemma codeNewVarCorrect (l : list nat) : codeNewVar (codeList l) = newVar l.
proof: Proof. unfold codeNewVar, newVar. set (f := fun n Hrecs : nat => switchPR n (Nat.max (S (car (pred n))) (codeNth (n - S (cdr (pred n))) Hrecs)) 0). induction l as [| a l Hrecl]. - simpl; unfold evalStrongRec; simpl; now rewrite cPairProjections1. - unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp; unfold compose2. unfold f at 1; rewrite evalStrongRecHelp1. + simpl; repeat rewrite cPairProjections1. rewrite <- Hrecl; repeat rewrite cPairProjections2. reflexivity. + simpl; repeat rewrite cPairProjections2. apply Nat.lt_succ_r, cPairLe2. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)