exists (λ x => ⟨⟨x, corec (bind.automaton k) (.inr x)⟩, by rfl⟩) <$> destruct x
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x)
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x