proposition: Lemma eqit_map {E R1 R2 S1 S2} (RR : R1 -> R2 -> Prop) b1 b2 (RS : S1 -> S2 -> Prop) f1 f2 t1 t2 : (forall r1 r2, RR r1 r2 -> RS (f1 r1) (f2 r2)) -> @eqit E _ _ RR b1 b2 t1 t2 -> eqit RS b1 b2 (ITree.map f1 t1) (ITree.map f2 t2).
proof: Proof. unfold ITree.map; intros. eapply eqit_bind'; eauto. intros; pstep; constructor; auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)