proposition: Theorem merge_olist: forall l1 l2, olist l1 -> olist l2 -> olist (merge l1 l2).
proof: Proof. intros l1; case l1; clear l1; simpl; auto. intros a l1 l2; case l2; simpl; auto; clear l2. intros; apply merge_olist_strong; auto. apply olist_one; auto. intros b l2 H H1. case_eq (weight a b); intros H2; auto. apply merge_olist_strong; auto. apply olist_cons; auto. apply merge_olist_strong; auto. rewrite weight_exact with (1 := H2); auto. generalize b H H1 H2; elim l2; simpl; auto; clear l2 b H H1 H2. intros b H H1 H2; apply olist_cons; auto. rewrite weight_anti_sym, H2; auto. apply merge_olist_strong; auto. apply olist_one; auto. intros b l2 Rec c H H1 H2. case_eq (weight a b); intros H3; auto. apply olist_cons; auto. rewrite weight_anti_sym; rewrite H2; auto. apply merge_olist_strong; auto. apply olist_cons; auto. apply olist_inv with (1 := H1); auto. apply olist_cons; auto. rewrite weight_anti_sym; rewrite H2; auto. apply merge_olist_strong; auto. rewrite weight_exact with (1 := H3); auto. apply olist_inv with (1 := H1); auto. apply olist_cons; auto. apply olist_weight with (1 := H1); auto with datatypes. apply Rec; auto. apply olist_inv with (1 := H1); auto. Qed.
imports: List Permutation UList