exact match l with
| [] => True.intro
| [t] => by
  simp only [andN, notList, map]
  simp only [orN, Not] at h
  exact h
| h₁::h₂::t => by
  simp only [orN, Not] at h
  have ⟨t₁, t₂⟩ := deMorganSmall h
  simp only [orN, Not] at t₂
  simp [andN, notList, map]
  have ih := @deMorgan₃ (h₂::t) t₂
  exact ⟨t₁, ih⟩
l : List Prop
h : ¬orN l
⊢ andN (notList l)
no goals