. constructor
case refl.refl.free.a.a.right
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).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
no goals