proposition: Lemma eqit_clo_trans b1 b2 vclo (MON: monotone2 vclo) (CMP: compose (eqitC b1 b2) vclo <3= compose vclo (eqitC b1 b2)): eqit_trans_clo b1 b2 false false <3= gupaco2 (eqit_ RR b1 b2 vclo) (eqitC b1 b2).
proof: Proof. intros. destruct PR. gclo. econstructor; eauto with paco. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)