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