apply pgfp.monotone ⟨eqF, eqF.monotone⟩ ⊥
case refl.refl.pure.a.h
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) })
    (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) x y
case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ⊥ ≤ fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z

case refl.refl.pure.a.h.a
F : Type u → Type u
inst : QPF F
R S T : Type u
k₁ : R → Free F S
k₂ : S → Free F T
y✝ z : Free F T
r : R
x y : Free F T
h : eq x y
⊢ ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥ x y