fact: Parameter instantiated_subterm : forall u u' sigma, trans_clos direct_subterm u u' -> trans_clos direct_subterm (apply_subst sigma u) (apply_subst sigma u').
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)