Theorem: disconEvalHT (Pdl/Discon.lean)

State before:
X : List Formula
⊢ ∀ (XS : List (List Formula)), discon (X :: XS)≡Con X⋁discon XS
Tactic:
unfold semEquiv
State after:
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)

State before:
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
Tactic:
intro XS W M w
State after:
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)

State before:
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (X :: XS)) ↔ evaluate M w (Con X⋁discon XS)
Tactic:
cases' XS with Y YS
State after:
case nil
X : List Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon [X]) ↔ evaluate M w (Con X⋁discon [])

case cons
X : List Formula
W : Type
M : KripkeModel W
w : W
Y : List Formula
YS : List (List Formula)
⊢ evaluate M w (discon (X :: Y :: YS)) ↔ evaluate M w (Con X⋁discon (Y :: YS))

State before:
case nil
X : List Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon [X]) ↔ evaluate M w (Con X⋁discon [])
Tactic:
simp
State after:
no goals

State before:
case cons
X : List Formula
W : Type
M : KripkeModel W
w : W
Y : List Formula
YS : List (List Formula)
⊢ evaluate M w (discon (X :: Y :: YS)) ↔ evaluate M w (Con X⋁discon (Y :: YS))
Tactic:
simp
State after:
no goals