proposition: Lemma LNN2LNT_exist (v : nat) (a : fol.Formula LNN) : LNN2LNT_formula (existH v a) = existH v (LNN2LNT_formula a).
proof: Proof. reflexivity. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)