Theorem: sat_negBigDis_iff_sat_bigConNeg (Bml/bigConDis.lean)

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