simp [*] at *
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
H1 : orN (qs.eraseIdx j) ∨ qs[j]
H2 : orN (ps.eraseIdx i) ∨ True
h : True
⊢ orN (qs.eraseIdx j)
ps qs : List Prop
i j : Nat
hi : i < ps.length
hj : j < qs.length
hps hqs : True
hij : ¬qs[j]
h : True
H1 : orN (qs.eraseIdx j)
H2 : True
⊢ orN (qs.eraseIdx j)