proposition: Lemma eutt_le_euttG rH rL gL gH: eutt RR <2= euttG rH rL gL gH.
proof: Proof. intros. econstructor. econstructor. apply rclo2_base. left. eapply paco2_mon_bot; eauto; intros. eapply eqitF_mono; eauto with paco. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)