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

State before:
l : List Prop
⊢ orN ((¬orN l) :: l)
Tactic:
cases l with
| nil => exact not_false
| cons l ls =>
  simp only [orN]
  apply cnfOrPos'
State after:
no goals

State before:
case nil

⊢ orN [¬orN []]
Tactic:
exact not_false
State after:
no goals

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

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