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