fact: Definition symb_sup_gen R1 R2 : relation symbol := fun f g => exists r, exists l, filter_top R1 (fun f' => f = f') r l /\ symb_in_term g r = true /\ defined R2 g.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)