proposition: Lemma SN_st u v : SN R u -> supterm u v -> SN R v.
proof: Proof. intros u_sn uv. eapply SN_incl. eapply incl_union_r. refl. eapply SN_inv. left. eapply t_step. apply uv. apply SN_supterm_R_mon. hyp. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)