simp only [eq_iff_iff, true_iff, iff_true, h, hqs, hij, hps] at *
case pos
ps qs : List Prop
i j : Nat
hps : orN ps
hqs : orN qs
hi : i < ps.length
hj : j < qs.length
hij : ps[i] = ¬qs[j]
H1 : (orN (qs.eraseIdx j) ∨ qs[j]) = orN qs
H2 : (orN (ps.eraseIdx i) ∨ ps[i]) = orN ps
h : ps[i]
⊢ orN (ps.eraseIdx i ++ qs.eraseIdx j)
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)