proposition: Lemma euttG_transD: forall rH rL gL gH t1 t2, transD RR (euttG rH rL gL gH) t1 t2 -> euttG rH rL gL gH t1 t2.
proof: Proof. econstructor. guclo eqit_clo_trans. destruct H. econstructor; eauto. edestruct REL; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)