proposition: Lemma supterm_R_mon_wf : WF R -> WF (supterm! U R).
proof: Proof. intro R_wf. apply Union.WF_union_commut. apply WF_tc. apply supterm_wf. hyp. apply commut_tc. apply supterm_R_mon_commut. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)