proposition: Lemma rutt_inv_Tau_r t1 t2 : rutt REv RAns RR t1 (Tau t2) -> rutt REv RAns RR t1 t2.
proof: Proof. intros. punfold H. red in H. simpl in *. pstep. red. remember (TauF t2) as tt2 eqn:Ett2 in H. revert t2 Ett2; induction H; try discriminate; intros; inversion Ett2; subst; auto. - pclearbot. constructor. pstep_reverse. - constructor. eapply IHruttF; eauto. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)