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