fact: Fixpoint occurs_in_term (v : variable) (t : term) {struct t} : Prop := match t with | Var v' => v=v' | Term _ l => let occurs_in_term_list := (fix occurs_in_term_list v (l : list _) {struct l} : Prop := match l with | nil => False | h :: tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl) end) in occurs_in_term_list v l end.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)