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