Theorem: sat_negBigCon_iff_sat_bigDisNeg (Bml/bigConDis.lean)

State before:
l : List Formula
⊢ Satisfiable (~bigCon l) ↔ Satisfiable (bigDis (List.map (fun x => ~x) l))
Tactic:
aesop
State after:
no goals