proposition: Lemma LNT2LNT_formula (f : Formula): LNN2LNT_formula (LNT2LNN_formula f) = f.
proof: Proof. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl. - now repeat rewrite LNT2LNT_term. - destruct r. - now rewrite Hrecf1, Hrecf0. - now rewrite Hrecf. - now rewrite Hrecf. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)