simp only [andN', impliesN]
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬andN' (p :: ps) ¬q → impliesN (p :: ps) q
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬(p ∧ andN' ps ¬q) → p → impliesN ps q