proposition: Lemma rclo_transD r: rclo2 (transD RR) r <2= @transD E R1 R2 RR r.
proof: Proof. intros. induction PR; eauto with paco. destruct IN. apply H in REL. destruct REL. econstructor; try apply REL; try eapply eqit_trans; eauto; auto_ctrans. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)