cases j with
| zero =>
  simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
  rw [or_comm]
| succ j =>
  simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
  congr
  rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
case cons
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < (t :: l).length
⊢ (orN ((t :: l).eraseIdx j) ∨ (t :: l)[j]) = orN (t :: l)
no goals