Theorem: disconEvalHT (Bml/bigConDis.lean)

State before:
X : List Formula
⊢ ∀ (XS : List (List Formula)), discon (X :: XS)≡bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon X⋁discon XS)
Tactic:
cases XS
<;> simp
State after:
no goals