fact: Definition filter_top R G : relation term := fun r l => R r l /\ match l with Var _ => False | Term f _ => G f end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)