Theorem: eval_neg_BigDis_iff_eval_bigConNeg (Bml/bigConDis.lean)

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