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

State before:
t : Prop
l : List Prop
⊢ orN (t :: l) = (t ∨ orN l)
Tactic:
cases l with
| nil => simp [orN]
| cons t' l => simp [orN]
State after:
no goals

State before:
case nil
t : Prop
⊢ orN [t] = (t ∨ orN [])
Tactic:
simp [orN]
State after:
no goals

State before:
case cons
t t' : Prop
l : List Prop
⊢ orN (t :: t' :: l) = (t ∨ orN (t' :: l))
Tactic:
simp [orN]
State after:
no goals