fact: Fixpoint varFormula (f : fol.Formula L) : list nat := match f with | equal t s => freeVarT t ++ freeVarT s | atomic r ts => freeVarTs ts | impH A B => varFormula A ++ varFormula B | notH A => varFormula A | forallH v A => v :: varFormula A end.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)