match l with
| []         => exact False.elim (h True.intro)
| [_]        => exact h
| p₁::p₂::ps => simp [orN, notList, map]
                match deMorganSmall₃ h with
                | Or.inl hnp₁ => exact Or.inl hnp₁
                | Or.inr hnAndTail =>
                  have IH := notAnd (p₂::ps) hnAndTail
                  exact Or.inr IH
l : List Prop
h : ¬andN l
⊢ orN (notList l)
no goals