proposition: Lemma SN_Inverse : forall a, (exists b, F a b /\ SN R b) -> SN RoF a.
proof: Proof. intros. destruct H as [b]. destruct H. eapply SN_RoF. apply H0. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)