proposition: Lemma Transitive_Roption : Transitive R -> Transitive Roption.
proof: Proof. clear. compute. intros. destruct H0; auto. inversion H1. constructor; auto. subst. eapply H; eassumption. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms ExtLib.Core.RelDec ExtLib.Structures.Reducible ExtLib.Structures.Traversable ExtLib.Structures.Applicative ExtLib.Structures.Functor ExtLib.Structures.FunctorLaws ExtLib.Data.Fun ExtLib.Tactics.Injection ExtLib.Tactics.Consider