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