apply bisim R
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
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