proposition: Lemma trans_rcompose {R} RR (TRANS: Transitive RR): forall x y : R, rcompose RR RR x y -> RR x y.
proof: Proof. intros. destruct H; eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)