fact: Fixpoint freeVarF (A : fol.Formula L) : list nat := match A with | equal t s => freeVarT t ++ freeVarT s | atomic r ts => freeVarTs _ ts | impH A B => freeVarF A ++ freeVarF B | notH A => freeVarF A | forallH v A => remove eq_nat_dec v (freeVarF A) end.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)