proposition: Lemma eqit_mon {E R1 R2} RR RR' (b1 b2 b1' b2': bool) (LEb1: b1 -> b1') (LEb2: b2 -> b2') (LERR: RR <2= RR'): @eqit E R1 R2 RR b1 b2 <2= eqit RR' b1' b2'.
proof: Proof. pcofix self. pstep. intros u v euv. punfold euv. red in euv |- *. induction euv; pclearbot; eauto 7 with paco itree. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)