apply eqF.Free
case refl.refl.free.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
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ eqF P (free ((flip bind k₂ ∘ flip bind k₁) <$> f)) (free (flip bind (flip bind k₂ ∘ k₁) <$> f))
case refl.refl.free.a.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
f : F (Free F R)
P : Free F T → Free F T → Prop := fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z
⊢ QPF.M.liftr F P ((flip bind k₂ ∘ flip bind k₁) <$> f) (flip bind (flip bind k₂ ∘ k₁) <$> f)