proposition: Lemma eqit_inv_Vis_weak {E R1 R2 RR} b1 b2 {u1 u2} (e1 : E u1) (e2 : E u2) (k1: u1 -> itree E R1) (k2: u2 -> itree E R2) : eqit RR b1 b2 (Vis e1 k1) (Vis e2 k2) -> exists p, eqeq E p e1 e2 /\ pweqeq (eqit RR b1 b2) p k1 k2.
proof: Proof. intros. punfold H; apply eqitF_inv_VisF_weak in H. destruct H as [ p []]. exists p; split; auto. revert H0; apply pweqeq_mon; intros; pclearbot; 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)