match l with
| [] => exact True.intro
| [p] =>
  match i with
  | 0 => exact h'
  | _ + 1 => exact True.intro
| p₁::p₂::ps =>
  match i with
  | 0 => exact And.left h'
  | i' + 1 =>
    have IH :=  cnfAndPos (p₂::ps) i'
    exact orImplies₂ IH (And.right h')
case a
l : List Prop
i : Nat
h : ¬¬andN l
h' : andN l
⊢ l.getD i True
no goals