apply @orN_subList qs (ps ++ qs) ps.length (ps.length + qs.length) hqs
qs ps : List Prop
hqs : orN qs
⊢ orN (ps ++ qs)
qs ps : List Prop
hqs : orN qs
⊢ qs = subList' (ps ++ qs) ps.length (ps.length + qs.length)