Theorem: subsetSat (Pdl/Semantics.lean)

State before:
W : Type
M : KripkeModel W
w : W
X Y : List Formula
⊢ (∀ φ ∈ X, evaluate M w φ) → Y ⊆ X → ∀ φ ∈ Y, evaluate M w φ
Tactic:
aesop
State after:
no goals