have := h hxz
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
⊢ z = y
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
h : ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
x y z : F.World
hxy : x = y
hxz : x ≺ z
this : x = z
⊢ z = y