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