apply orN_append_right (by simp [*] at *; exact H1)
case pos
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 (ps.eraseIdx i ++ qs.eraseIdx j)
no goals