apply orN_append_left H2
case neg
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)
h : True
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
no goals