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