fact: Parameter acc_with_subterm_subterms : forall R t, Acc (union _ (one_step R) direct_subterm) t -> forall s, direct_subterm s t -> Acc (union _ (one_step R) direct_subterm) s.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)