proposition: Lemma eqitC_mon b1 b2 r1 r2 t1 t2 (IN: eqitC b1 b2 r1 t1 t2) (LE: r1 <2= r2): eqitC b1 b2 r2 t1 t2.
proof: Proof. destruct IN. econstructor; eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)