proposition: Lemma SN_supterm_R_mon : forall u, SN R u -> SN (supterm! U R) u.
proof: Proof. intros u hu. apply Union.SN_union_commut. intros x _. apply WF_tc. apply supterm_wf. hyp. apply tc_supterm_R_mon_commut. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)