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