simp
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 = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
a : M F
⊢ (construct (destruct a), a).fst = construct (destruct (construct (destruct a), a).snd)
no goals