proposition: Lemma LNN2LNT_natToTerm (n:nat): LNN2LNT_term (natToTermLNN n) = natToTerm 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)