proposition: Lemma WF_compat_inv : WF R -> WF (R @ E).
proof: Proof. unfold WF. intros. ded (H x). elim H0. intros. apply SN_intro. intros. do 2 destruct H3. ded (H2 _ H3). apply (SN_compat_inv H5 H4). Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)