simp [orN, notList, map]
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ orN (notList (p₁ :: p₂ :: ps))
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)