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