apply h₂
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
F : Type u → Type u
inst : QPF F
R S T : Type u
t : Free F R
k₁ : R → Free F S
k₂ : S → Free F T
h₁ :
  (fun y z => ∃ x, x >>= k₁ >>= k₂ = y ∧ x >>= flip bind k₂ ∘ k₁ = z) (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) ≤
    eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)
h₂ : eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁) → t >>= k₁ >>= k₂ = t >>= flip bind k₂ ∘ k₁
⊢ eq (t >>= k₁ >>= k₂) (t >>= flip bind k₂ ∘ k₁)