match l with
| [] => exact False.elim p
| [h] =>
  match i with
  | 0 => exact absurd p orNl
  | _ + 1 => exact False.elim p
| h₁::h₂::hs =>
  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
case a
l : List Prop
i : Nat
orNl : ¬orN l
p : l.getD i False
andNotl : andN (notList l)
⊢ False
no goals