rw [length_cons, succ_lt_succ_iff] at hj
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
⊢ j < l.length
t : Prop
l : List Prop
ih : ∀ {j : Nat} (hj : j < l.length), (orN (l.eraseIdx j) ∨ l[j]) = orN l
j : Nat
hj : j < l.length
⊢ j < l.length