proposition: Lemma ruttF_inv_VisF_r {sim} t1 U2 (e2: E2 U2) (k2: U2 -> _): ruttF sim t1 (VisF e2 k2) -> (exists U1 (e1: E1 U1) k1, t1 = VisF e1 k1 /\ forall v1 v2, RAns e1 v1 e2 v2 -> sim (k1 v1) (k2 v2)) \/ (exists t1', t1 = TauF t1' /\ ruttF sim (observe t1') (VisF e2 k2)).
proof: Proof. refine (fun H => match H in ruttF _ _ 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(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)