proposition: Lemma euttG_tau: forall rH rL gL gH t1 t2, euttG rH gL gL gH t1 t2 -> euttG rH rL gL gH (Tau t1) (Tau t2).
proof: Proof. intros. apply euttG_gen. destruct H. econstructor. gstep. econstructor. eapply gpaco2_mon; eauto; intros; repeat destruct PR as [PR|PR]; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)