exact match l with
| [] => by
  simp [orN, notList]
| [t] => by
  simp only [orN, notList]
  simp [andN] at h
  exact notNotIntro h
| h₁::h₂::t => by
  simp only [orN, notList, map]
  simp [andN] at h
  apply deMorganSmall₂
  have nnh₁ := notNotIntro (And.left h)
  have ih := @deMorgan₂ (h₂::t) (And.right h)
  exact ⟨nnh₁, ih⟩
l : List Prop
h : andN l
⊢ ¬orN (notList l)
no goals