proposition: Lemma LNT2LNN_natToTerm (n: nat) : LNT2LNN_term (natToTerm n) = natToTermLNN n.
proof: Proof. induction n as [| n Hrecn]. - reflexivity. - simpl; now rewrite Hrecn. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)