proposition: Lemma WF_Inverse : WF R -> WF RoF.
proof: Proof. unfold WF. intros H a. apply SN_intro. intros a' H'. destruct H' as [b']. destruct H0. apply (@SN_RoF b'). apply H. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)