sorted q2_lt l1 → (\snd (\last ▭ l1) = 〈OQ,OQ〉) →
sorted q2_lt l2 → (\snd (\last ▭ l2) = 〈OQ,OQ〉) →
rebase_spec_aux_p l1 l2 p.
sorted q2_lt l1 → (\snd (\last ▭ l1) = 〈OQ,OQ〉) →
sorted q2_lt l2 → (\snd (\last ▭ l2) = 〈OQ,OQ〉) →
rebase_spec_aux_p l1 l2 p.