- [ nil ⇒ 〈mk_list (λi.〈fst (nth l2 q00 i),OQ〉) (length ? l2),l2〉
- | cons he tl ⇒ 〈[],[]〉] in aux);
+ [ nil ⇒
+ let copy_l2_with_0 ≝ mk_list (λi.〈fst (nth l2 q0 i),OQ〉) (length ? l2) in
+ 〈copy_l2_with_0, l2〉
+ | cons he1 tl1 ⇒〈[],[]〉 (*
+ match l2 with
+ [ nil ⇒
+ let copy_l1_with_0 ≝ mk_list (λi.〈fst (nth l1 q0 i),OQ〉) (length ? l1) in
+ 〈l1, copy_l1_with_0〉
+ | 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_eq _ ⇒
+ let rc ≝ aux tl1 tl2 m in
+ 〈he1 :: fst rc,he2 :: snd rc〉
+ | q_lt _ ⇒
+ let rest ≝ base2 - base1 in
+ let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
+ 〈〈base1,height1〉 :: fst rc,〈base1,height2〉 :: snd rc〉
+ | q_gt _ ⇒
+ 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.∃p.True);