fact: Definition LTFormula := (exH 2, v#0 + LNT.Succ v#2 = v#1)%nt.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)