proposition: Lemma eq_inv_VisF_weak {E R X1 X2} (e1 : E X1) (e2 : E X2) (k1 : X1 -> itree E R) (k2 : X2 -> itree E R) : VisF (R := R) e1 k1 = VisF (R := R) e2 k2 -> exists p : X1 = X2, eqeq E p e1 e2 /\ eqeq (fun X => X -> itree E R) p k1 k2.
proof: Proof. refine (fun H => match H in _ = t return match t with | VisF e2 k2 => _ | _ => True end with | eq_refl => _ end); cbn. exists eq_refl; cbn; auto. Qed.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)