proposition: Lemma rutt_Vis {T1 T2} (e1: E1 T1) (e2: E2 T2) (k1: T1 -> itree E1 R1) (k2: T2 -> itree E2 R2): REv _ _ e1 e2 -> (forall t1 t2, RAns _ _ e1 t1 e2 t2 -> rutt REv RAns RR (k1 t1) (k2 t2)) -> rutt REv RAns RR (Vis e1 k1) (Vis e2 k2).
proof: Proof. intros He Hk. pstep; constructor; auto. intros; left. apply Hk; auto. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)