proposition: Lemma restrict_SN_clos_aeq_tc_supterm_acc_R_mon_wf : WF (restrict (SN R) (clos_aeq (supterm_acc!) U R)).
proof: Proof. apply restrict_clos_aeq_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)