proposition: Lemma euttG_accF rH rL gL gH X (f : X -> _) (g : X -> _) (OBJ: forall gL' (INCL: gL <2= gL') (CIHL: forall x : X, gL' (f x) (g x)) gH' (INCH: gH <2= gH') (CIHH: forall x : X, gH' (f x) (g x)), forall x : X, euttG rH rL gL' gH' (f x) (g x)): forall x : X, euttG rH rL gL gH (f x) (g x).
proof: Proof. intros x. apply euttG_cofix with (x := fun a b => exists x, a = (f x) /\ b = (g x)); [ | eauto ]. intros. destruct PR as [? [-> ->]]. apply OBJ; eauto. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)