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