proposition: Lemma codeNatToTermCorrectLNT n : codeNatToTerm n = codeTerm (natToTermLNT n).
proof: Proof. induction n as [| n Hrecn]. - reflexivity. - simpl; now rewrite Hrecn. Qed.
imports: hydras.Ackermann(primRec cPair code folProp folProof Languages) Coq(Arith)