Theorem: conEvalHT (Bml/bigConDis.lean)

State before:
X : List Formula
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon (f :: X)) ↔ Evaluate (M, w) f ∧ Evaluate (M, w) (bigCon X)
Tactic:
cases X
<;> simp
State after:
no goals