proposition: Lemma eqit_Tau b1 b2 (t1 : itree E R1) (t2 : itree E R2) : eqit RR b1 b2 (Tau t1) (Tau t2) <-> eqit RR b1 b2 t1 t2.
proof: Proof. split; intros H. - punfold H. red in H. simpl in *. pstep. red. remember (TauF t1) as ot1. remember (TauF t2) as ot2. hinduction H before RR; intros; subst; try inv Heqot1; try inv Heqot2; eauto. + pclearbot. punfold REL. + inv H; eauto with itree. + inv H; eauto with itree. - pstep. constructor; auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)