fact: Definition inner (R : relation term) (t : term) := forall s, direct_subterm s t -> nf (one_step R) s.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)