exists inst.map (λ x => ⟨⟨x >>= k₁ >>= k₂, x >>= (flip bind k₂ ∘ k₁)⟩, by exists x⟩) 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)
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
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
              property :=
                (_ :
                  ∃ x_1,
                    x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                      x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
          f =
      (flip bind k₂ ∘ flip bind k₁) <$> f ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁),
              property :=
                (_ :
                  ∃ x_1,
                    x_1 >>= k₁ >>= k₂ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).fst ∧
                      x_1 >>= flip bind k₂ ∘ k₁ = (x >>= k₁ >>= k₂, x >>= flip bind k₂ ∘ k₁).snd) }) <$>
          f =
      flip bind (flip bind k₂ ∘ k₁) <$> f