proposition: Lemma rutt_inv_Ret r1 r2: rutt REv RAns RR (Ret r1) (Ret r2) -> RR r1 r2.
proof: Proof. intros. punfold H. inv H. eauto. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)