fact: Definition UsableRules (R C : relation term) : relation term := fun u v => exists r, exists l, C r l /\ Usable R r u v.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)