proposition: Lemma eqitF_inv_VisF_weak {E R1 R2} (RR : R1 -> R2 -> Prop) {b1 b2 vclo sim} X1 (e1 : E X1) (k1 : X1 -> _) X2 (e2 : E X2) (k2 : X2 -> _) : eqitF RR b1 b2 vclo sim (VisF e1 k1) (VisF e2 k2) -> exists p : X1 = X2, eqeq E p e1 e2 /\ pweqeq (vclo sim) p k1 k2.
proof: Proof. refine (fun H => match H in eqitF _ _ _ _ _ t1 t2 return match t1, t2 return Prop with | VisF e1 k1, VisF e2 k2 => _ | _, _ => True end with | EqVis _ _ _ _ _ _ _ _ _ => _ | _ => _ end); try exact I. - exists eq_refl; cbn; eauto. - destruct i; exact I. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)