proposition: Lemma rclo_flip clo (r: itree E R1 -> itree E R2 -> Prop) (MON: monotone2 clo): flip (rclo2 (fun x : itree E R2 -> itree E R1 -> Prop => flip (clo (flip x))) (flip r)) <2= rclo2 clo r.
proof: Proof. intros. induction PR; eauto with paco. apply rclo2_clo; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)