simp only [pure_bind, flip, Function.comp]
case refl.refl.pure
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
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z)
    (pure r >>= k₁ >>= k₂) (pure r >>= flip bind k₂ ∘ k₁)
case refl.refl.pure
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
⊢ eqF
    ((fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z) ⊔
      ↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) fun y z =>
        ∃ x, x >>= k₁ >>= k₂ = y ∧ (x >>= fun x => k₁ x >>= k₂) = z)
    (k₁ r >>= k₂) (k₁ r >>= k₂)