proposition: Lemma rutt_inv_Ret_r t1 r2: rutt REv RAns RR t1 (Ret r2) -> exists r1, t1 ≳ Ret r1 /\ RR r1 r2.
proof: Proof. intros Hrutt; punfold Hrutt; red in Hrutt; cbn in Hrutt. setoid_rewrite (itree_eta t1). remember (RetF r2) as ot2; revert Heqot2. induction Hrutt; intros; try discriminate. - inversion Heqot2; subst. exists r1. split; [reflexivity|auto]. - destruct (IHHrutt Heqot2) as [r1 [H1 H2]]. exists r1; 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)