proposition: Lemma euttG_cofix rH rL gL gH x (OBG: forall gL' (INCL: gL <2= gL') (CIHL: x <2= gL') gH' (INCH: gH <2= gH') (CIHH: x <2= gH'), x <2= euttG rH rL gL' gH'): x <2= euttG rH rL gL gH.
proof: Proof. eapply euttG_cofix_aux; intros. eapply OBG; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)