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