fact: Fixpoint LNT2LNN_formula (f : Formula) : fol.Formula LNN := match f with | (t1 = t2)%nt => (LNT2LNN_term t1 = LNT2LNN_term t2)%fol | atomic r ts => match r with end | (A -> B)%nt => (LNT2LNN_formula A -> LNT2LNN_formula B)%fol | (~ A)%nt => (~ LNT2LNN_formula A)%fol | (allH v, A)%nt => (allH v, LNT2LNN_formula A)%fol end.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)