intro hnpps hp
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬(p ∧ andN' ps ¬q) → p → impliesN ps q
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
⊢ impliesN ps q