proposition: Lemma ruttF_inv_VisF {sim} U1 U2 (e1 : E1 U1) (e2 : E2 U2) (k1 : U1 -> _) (k2 : U2 -> _) : ruttF sim (VisF e1 k1) (VisF e2 k2) -> forall v1 v2, RAns e1 v1 e2 v2 -> sim (k1 v1) (k2 v2).
proof: Proof. intros H. dependent destruction H. assumption. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)