simp_all [Satisfies]
case hand
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⋏ q✝) → Satisfies M w' (p✝ ⋏ q✝)
no goals