proposition: Lemma restrict_SN_tc_supterm_acc_R_mon_wf : WF (restrict (SN R) (supterm_acc! U R)).
proof: Proof. apply restrict_tc_supterm_acc_R_mon_wf. class. apply wf_restrict_sn. refl. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)