unfold andN
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ andN (p₁ :: p₂ :: ps) → q
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q