proposition: Lemma restrict_SN_tc_supterm_R_mon_wf : WF (restrict (SN R) (supterm! U R)).
proof: Proof. apply restrict_tc_supterm_R_mon_wf. intros u u' uu' h. eapply SN_inv. apply uu'. hyp. apply wf_restrict_sn. refl. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)