proposition: Lemma codeLengthCorrect : forall l : list nat, codeLength (codeList l) = length l.
proof: Proof. induction l as [| a l Hrecl]. - reflexivity. - simpl; unfold codeLength. set (f := fun n Hrecs : nat => switchPR n (S (codeNth (n - S (cPairPi2 (pred n))) Hrecs)) 0) in *. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalList, f. rewrite evalStrongRecHelp1; simpl. + rewrite cPairProjections1. apply eq_S. rewrite cPairProjections2; apply Hrecl; simpl. + apply Compat815.le_lt_n_Sm. generalize (cPair a (codeList l)); intro n. apply Nat.le_trans with (cPair (cPairPi1 n) (cPairPi2 n)). * apply cPairLe2. * rewrite cPairProjections; apply le_n. Qed.
imports: hydras.Ackermann(primRec cPair) hydras.Ackermann(ListExt) Coq(Arith) hydras(extEqualNat Compat815)