rw [eq, eqP, ←pgfp.unfold, CompleteLattice.bot_sup] at this
case refl.refl.pure.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
this : eq (k₁ r >>= k₂) (k₁ r >>= k₂)
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)
case refl.refl.pure.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
this :
  ↑{ toFun := eqF, monotone' := (_ : Monotone eqF) } (↑(pgfp { toFun := eqF, monotone' := (_ : Monotone eqF) }) ⊥)
    (k₁ r >>= k₂) (k₁ r >>= k₂)
⊢ eqF eq (k₁ r >>= k₂) (k₁ r >>= k₂)