simp [liftr]
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
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ liftr F R (destruct x) (destruct y)
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
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y