proposition: Lemma eqit_idclo_compat b1 b2: compose (eqitC b1 b2) id <3= compose id (eqitC b1 b2).
proof: Proof. intros. apply PR. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)