. intro h x y hyz;
  have := h rfl hyz;
  subst this;
  trivial;
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y

case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y