proposition: Lemma rutt_inv_Vis_l {U1} (e1: E1 U1) k1 t2: rutt REv RAns RR (Vis e1 k1) t2 -> exists U2 (e2: E2 U2) k2, t2 ≈ Vis e2 k2 /\ REv _ _ e1 e2 /\ (forall v1 v2, RAns _ _ e1 v1 e2 v2 -> rutt REv RAns RR (k1 v1) (k2 v2)).
proof: Proof. intros Hrutt; punfold Hrutt; red in Hrutt; cbn in Hrutt. setoid_rewrite (itree_eta t2). remember (VisF e1 k1) as ot1; revert Heqot1. induction Hrutt; intros; try discriminate; subst. - inversion Heqot1; subst A. inversion_sigma; rewrite <- eq_rect_eq in *; subst; rename B into U2. exists U2, e2, k2; split. reflexivity. split; auto. intros v1 v2 HAns. specialize (H0 v1 v2 HAns). red in H0. now pclearbot. - destruct (IHHrutt eq_refl) as (U2 & e2 & k2 & Ht0 & HAns). rewrite <- itree_eta in Ht0. exists U2, e2, k2; split; auto. now rewrite tau_eutt. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)