include "russell_support.ma".
include "models/q_copy.ma".
-
+(*
definition rebase_spec ≝
λl1,l2:q_f.λp:q_f × q_f.
And3
whd; rewrite < H6; apply (inversion_sorted2 ??? H5);
| apply (sorted_one q2_lt);]
qed.
+*)
+
+
definition rebase_spec_aux ≝
- λl1,l2:list bar.λp:(list bar) × (list bar).
+ λl1,l2
+ :list bar.λp:(list bar) × (list bar).
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.