proposition: Lemma rutt_inv_Vis U1 U2 (e1: E1 U1) (e2: E2 U2) (k1: U1 -> itree E1 R1) (k2: U2 -> itree E2 R2): rutt REv RAns RR (Vis e1 k1) (Vis e2 k2) -> forall u1 u2, RAns U1 U2 e1 u1 e2 u2 -> rutt REv RAns RR (k1 u1) (k2 u2).
proof: Proof. intros H u1 u2 Hans. punfold H. apply ruttF_inv_VisF with (v1 := u1) (v2 := u2) in H. pclearbot; auto. assumption. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)