proposition: Lemma eqit_inv_Tau_r {E R1 R2 RR} b2 t1 t2 : @eqit E R1 R2 RR true b2 t1 (Tau t2) -> eqit RR true b2 t1 t2.
proof: Proof. intros. punfold H. red in H. simpl in *. remember (TauF t2) as tt2. genobs t1 ot1. hinduction H before b2; intros; try discriminate. - inv Heqtt2. pclearbot. pstep. red. simpobs. econstructor; eauto. pstep_reverse. - red in IHeqitF. pstep. red; simpobs. econstructor; eauto. pstep_reverse. - inv Heqtt2. punfold_reverse H. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)