proposition: Lemma instantiated_subterm : forall u u' sigma, trans_clos direct_subterm u u' -> trans_clos direct_subterm (apply_subst sigma u) (apply_subst sigma u').
proof: Proof. intros u u' sigma; apply trans_incl2. intros s [ | f l] s_in_l. contradiction. simpl; rewrite in_map_iff; exists s; split; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)