Theorem: eval_negBigCon_iff_eval_bigDisNeg (Bml/bigConDis.lean)

State before:
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (~bigCon l) ↔ Evaluate (M, w) (bigDis (List.map (fun x => ~x) l))
Tactic:
aesop
State after:
no goals