. intro x y h₀
  have h₀ := congrArg destruct h₀
  simp [liftr]
  simp only [construct, destruct_corec, construct.automaton] at h₀
  exists Functor.map (λ a => ⟨⟨construct <| destruct a, a⟩, by simp⟩) (destruct y)
  rw [h₀]
  constructor
  . simp only [←QPF.map_comp]
    rfl
  . rw [←QPF.M.map_comp]
    have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
    apply Eq.trans _ this
    apply congrFun
    funext _
    rfl
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)

case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x