proposition: Lemma rutt_inv_Ret_l r1 t2: rutt REv RAns RR (Ret r1) t2 -> exists r2, t2 ≳ Ret r2 /\ RR r1 r2.
proof: Proof. intros Hrutt; punfold Hrutt; red in Hrutt; cbn in Hrutt. setoid_rewrite (itree_eta t2). remember (RetF r1) as ot1; revert Heqot1. induction Hrutt; intros; try discriminate. - inversion Heqot1; subst. exists r2. split; [reflexivity|auto]. - destruct (IHHrutt Heqot1) as [r2 [H1 H2]]. exists r2; split; auto. rewrite <- itree_eta in H1. now rewrite tau_euttge. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)