induction qs with
| nil =>
  intro j hj
  simp at hj; exfalso
  exact not_succ_le_zero j hj
| cons t l ih =>
  intro j hj
  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)]
qs : List Prop
⊢ ∀ {j : Nat} (hj : j < qs.length), (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
no goals