cases hCon ⟨rxy, rxz⟩ with
| inl ryz =>
  have := hyp _ ryz;
  simp_all only [Satisfies.imp_def, implies_true];
| inr rzy =>
  simp [Satisfies.box_def, Satisfies.imp_def]
  intro hq;
  have hyp := hq y rzy;
  contradiction;
case intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
no goals