induction ps with
| nil => exact notNotElim
| cons p ps ih =>
  simp only [andN', impliesN]
  intro hnpps hp
  have hnpnps := deMorganSmall₃ hnpps
  match hnpnps with
  | .inl hnp => contradiction
  | .inr hnps => exact ih hnps
ps : List Prop
q : Prop
⊢ ¬andN' ps ¬q → impliesN ps q
no goals