proposition: Lemma eqit_Tau_r {E R1 R2 RR} b1 (t1 : itree E R1) (t2 : itree E R2) : eqit RR b1 true t1 t2 -> eqit RR b1 true t1 (Tau t2).
proof: Proof. intros. pstep. econstructor; eauto. punfold 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)