Theorem: Smt.Reconstruct.Prop.cnfAndNeg (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
l : List Prop
⊢ orN (andN l :: notList l)
Tactic:
cases l with
| nil => trivial
| cons l ls =>
  simp only [orN]
  apply cnfAndNeg'
State after:
no goals

State before:
case nil

⊢ orN (andN [] :: notList [])
Tactic:
trivial
State after:
no goals

State before:
case cons
l : Prop
ls : List Prop
⊢ orN (andN (l :: ls) :: notList (l :: ls))
Tactic:
simp only [orN]
State after:
case cons
l : Prop
ls : List Prop
⊢ andN (l :: ls) ∨ orN ((¬l) :: map Not ls)

State before:
case cons
l : Prop
ls : List Prop
⊢ andN (l :: ls) ∨ orN ((¬l) :: map Not ls)
Tactic:
apply cnfAndNeg'
State after:
no goals