exact match l with
| []   => True.intro
| [t]  => by
  simp only [andN]
  simp only [notList, orN, map] at h
  cases Classical.em t with
  | inl tt  => exact tt
  | inr ntt => exact False.elim (h ntt)
| h₁::h₂::t => by
  simp only [orN, notList, map] at h
  have ⟨ t₁, t₂ ⟩ := deMorganSmall h
  have ih := @deMorgan (h₂::t) t₂
  simp [andN]
  have t₁' := notNotElim t₁
  exact ⟨ t₁', ih ⟩
l : List Prop
h : ¬orN (notList l)
⊢ andN l
no goals