have ih := @deMorgan₂ (h₂::t) (And.right h)
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
ih : ¬orN (notList (h₂ :: t))
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)