+lemma copy_rebases:
+ ∀l1.rebase_spec_aux l1 [] 〈l1, copy l1〉.
+intros; elim l1; intros 4;
+[1: split; [left; reflexivity]; split; try assumption; unfold; intros;
+ unfold same_values; intros; reflexivity;
+|2: rewrite > H3; [2: intro X; destruct X]
+ split; [left; reflexivity] split;
+ unfold same_values_simpl; unfold same_values; intros; try reflexivity;
+ try assumption; [4: normalize in p2; destruct p2|2: cases H5; reflexivity;]
+ [1: apply (sorted_copy ? H1);
+ |2: apply (copy_same_bases (a::l));]]
+qed.
+
+lemma copy_rebases_r:
+ ∀l1.rebase_spec_aux [] l1 〈copy l1, l1〉.
+intros; elim l1; intros 4;
+[1: split; [left; reflexivity]; split; try assumption; unfold; intros;
+ unfold same_values; intros; reflexivity;
+|2: rewrite > H4; [2: intro X; destruct X]
+ split; [right; simplify; rewrite < minus_n_n; reflexivity] split;
+ unfold same_values_simpl; unfold same_values; intros; try reflexivity;
+ try assumption; [4: normalize in p2; destruct p2|2: cases H5; reflexivity;]
+ [1: apply (sorted_copy ? H2);
+ |2: intro; symmetry; apply (copy_same_bases (a::l));]]
+qed.
+
+definition rebase: ∀l1,l2:q_f.∃p:q_f × q_f.rebase_spec l1 l2 p.
+intros 2 (f1 f2); cases f1 (b1 Hs1 Hb1 He1); cases f2 (b2 Hs2 Hb2 He2); clear f1 f2;
+alias symbol "plus" = "natural plus".
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
+alias symbol "minus" = "Q minus".
+letin aux ≝ (
+let rec aux (l1,l2:list bar) (n : nat) on n : (list bar) × (list bar) ≝
+match n with
+[ O ⇒ 〈[], []〉
+| S m ⇒
+ match l1 with
+ [ nil ⇒ 〈copy l2, l2〉
+ | cons he1 tl1 ⇒
+ match l2 with
+ [ nil ⇒ 〈l1, copy l1〉
+ | cons he2 tl2 ⇒
+ let base1 ≝ \fst he1 in
+ let base2 ≝ \fst he2 in
+ let height1 ≝ \snd he1 in
+ let height2 ≝ \snd he2 in
+ match q_cmp base1 base2 with
+ [ q_leq Hp1 ⇒
+ match q_cmp base2 base1 with
+ [ q_leq Hp2 ⇒
+ let rc ≝ aux tl1 tl2 m in
+ 〈he1 :: \fst rc,he2 :: \snd rc〉
+ | q_gt Hp ⇒
+ let rest ≝ base2 - base1 in
+ let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
+ 〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉]
+ | q_gt Hp ⇒
+ let rest ≝ base1 - base2 in
+ let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
+ 〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉]]]]
+in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z);
+[7: clearbody aux; cases (aux b1 b2 (\len b1 + \len b2)) (w Hw); clear aux;
+ cases (Hw (le_n ?) Hs1 Hs2 (λ_.He1) (λ_.He2)); clear Hw; cases H1; cases H2; cases H3; clear H3 H1 H2;
+ exists [constructor 1;constructor 1;[apply (\fst w)|5:apply (\snd w)]] try assumption;
+ [1,3: apply hide; cases H (X X); try rewrite < (H8 O); try rewrite < X; assumption
+ |2,4: apply hide;[apply H6|apply H7]intro X;[rewrite > X in Hb1|rewrite > X in Hb2]
+ normalize in Hb1 Hb2; [destruct Hb1|destruct Hb2]]
+ unfold; unfold same_values; simplify in ⊢ (? (? % %) ? ?);
+ simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉);
+ split; [assumption; |apply H9;|apply H10]
+|6: intro ABS; unfold; intros 4; clear H1 H2;
+ cases l in ABS H3; intros 1; [2: simplify in H1; cases (not_le_Sn_O ? H1)]
+ cases l1 in H4 H1; intros; [2: simplify in H2; cases (not_le_Sn_O ? H2)]
+ split; [ left; reflexivity|split; apply (sorted_nil q2_lt);|split; assumption;]
+ split; unfold; intros; unfold same_values; intros; reflexivity;
+|5: intros; apply copy_rebases_r;
+|4: intros; rewrite < H1; apply copy_rebases;
+|3: cut (\fst b = \fst b3) as K; [2: apply q_le_to_le_to_eq; assumption] clear H6 H5 H4 H3;
+ intros; cases (aux l2 l3 n1); intros 4; simplify in match (\fst ≪w,H≫);
+ simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉);
+ cases H4;
+ [2: apply le_S_S_to_le; apply (trans_le ???? H3); simplify;
+ rewrite < plus_n_Sm; apply le_S; apply le_n;
+ |3,4: apply (sorted_tail q2_lt); [2: apply H5|4:apply H6]
+ |5: intro; cases l2 in H7 H9; intros; [cases H9; reflexivity]
+ simplify in H7 ⊢ %; apply H7; intro; destruct H10;
+ |6: intro; cases l3 in H8 H9; intros; [cases H9; reflexivity]
+ simplify in H8 ⊢ %; apply H8; intro; destruct H10;]
+ clear aux; split;
+ [1: left; reflexivity;
+ |2: cases H10;