fact: Fixpoint defined_list (l : list (term * term)) acc := match l with | nil => acc | (Var _, _) :: tl => defined_list tl acc | (Term f _, _) :: tl => defined_list tl (f :: acc) end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)