simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN ((t :: l).eraseIdx 0) ∨ (t :: l)[0]) = orN (t :: l)
case cons.zero
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
hj : 0 < (t :: l).length
⊢ (orN l ∨ t) = (t ∨ orN l)