have ⟨t₁, t₂⟩ := deMorganSmall h
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
⊢ andN (notList (h₁ :: h₂ :: t))
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : ¬orN (h₂ :: t)
⊢ andN (notList (h₁ :: h₂ :: t))