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