fact: Fixpoint freeVarT (s : fol.Term L) : list nat := match s with | var v => v :: nil | apply f ts => freeVarTs (arityF L f) ts end with freeVarTs (n : nat) (ss : fol.Terms L n) {struct ss} : list nat := match ss with | Tnil => nil (A:=nat) | Tcons m t ts => freeVarT t ++ freeVarTs m ts end.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)