proposition: Lemma eqitF_mono b1 b2 x0 x1 vclo vclo' sim sim' (IN: eqitF b1 b2 vclo sim x0 x1) (MON: monotone2 vclo) (LEc: vclo <3= vclo') (LE: sim <2= sim'): eqitF b1 b2 vclo' sim' x0 x1.
proof: Proof. intros. induction IN; eauto with 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)