proposition: Lemma restrict_tc_supterm_R_mon_wf : WF (restrict P R) -> WF (restrict P (supterm! U R)).
proof: Proof. intro h. rewrite restrict_union. apply Union.WF_union_commut. apply wf_restrict_sn. intros t ht. apply WF_tc. apply supterm_wf. hyp. intros t v [u [[ht tu] [hu uv]]]. assert (a : (supterm! @ R) t v). exists u. fo. destruct (tc_supterm_R_mon_commut a) as [u' [tu' u'v]]. exists u'. split; split; auto. eapply P_R. apply tu'. hyp. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)