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

State before:
⊢ ∀ (l : List Prop), andN l ∨ orN (notList l)
Tactic:
intro l
State after:
l : List Prop
⊢ andN l ∨ orN (notList l)

State before:
l : List Prop
⊢ andN l ∨ orN (notList l)
Tactic:
apply orComm
State after:
case a
l : List Prop
⊢ orN (notList l) ∨ andN l

State before:
case a
l : List Prop
⊢ orN (notList l) ∨ andN l
Tactic:
apply orImplies
State after:
case a.a
l : List Prop
⊢ ¬orN (notList l) → andN l

State before:
case a.a
l : List Prop
⊢ ¬orN (notList l) → andN l
Tactic:
intro h
State after:
case a.a
l : List Prop
h : ¬orN (notList l)
⊢ andN l

State before:
case a.a
l : List Prop
h : ¬orN (notList l)
⊢ andN l
Tactic:
exact deMorgan h
State after:
no goals