Theorem: disconEval (Pdl/Discon.lean)

State before:
W : Type
M : KripkeModel W
w : W
⊢ ∀ (XS : List (List Formula)), evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
intro XS
State after:
W : Type
M : KripkeModel W
w : W
XS : List (List Formula)
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
XS : List (List Formula)
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
apply disconEval' XS rfl
State after:
no goals