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
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
no goals