proposition: Lemma clos_aeq_tc_supterm_acc_R_mon_wf : WF R -> WF (clos_aeq (supterm_acc!) U R).
proof: Proof. intro R_wf. apply Union.WF_union_commut. apply clos_aeq_tc_supterm_acc_wf. hyp. apply clos_aeq_tc_supterm_acc_R_mon_commut. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)