proposition: Lemma rutt_inv_Tau_l t1 t2 : rutt REv RAns RR (Tau t1) t2 -> rutt REv RAns RR t1 t2.
proof: Proof. intros. punfold H. red in H. simpl in *. remember (TauF t1) as tt1. genobs t2 ot2. hinduction H before t1; intros; try discriminate. - inv Heqtt1. pclearbot. pstep. red. simpobs. econstructor; eauto. pstep_reverse. - inv Heqtt1. punfold_reverse H. - red in IHruttF. pstep. red; simpobs. econstructor; eauto. pstep_reverse. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)