exact absurd orNTail notOrNTail
l : List Prop
i : Nat
h₁ h₂ : Prop
hs : List Prop
orNl : ¬orN (h₁ :: h₂ :: hs)
andNotl : andN (notList (h₁ :: h₂ :: hs))
i' : Nat
p : (h₁ :: h₂ :: hs).getD (i' + 1) False
IH : orN (h₂ :: hs) ∨ ¬(h₂ :: hs).getD i' False
orNTail : orN (h₂ :: hs)
left✝ : ¬h₁
notOrNTail : ¬orN (h₂ :: hs)
⊢ False
no goals