match i with
| 0 => have ⟨nh₁p, _⟩ := andNotl
       exact absurd p nh₁p
| i' + 1 =>
  have IH := cnfOrNeg (h₂::hs) i'
  have orNTail := orImplies₂ (orComm IH) p
  have ⟨_, notOrNTail⟩ := deMorganSmall orNl
  exact absurd orNTail notOrNTail
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
p : (h₁ :: h₂ :: hs).getD i False
andNotl : andN (notList (h₁ :: h₂ :: hs))
⊢ False
no goals