proposition: Theorem merge_incl_r: forall l1 l2, incl l2 (merge l1 l2).
proof: Proof. intros l1; elim l1; simpl; auto with datatypes. intros a l3 Rec l2; elim l2; simpl; auto with datatypes; clear l2. intros b l2 Rec1; case_eq (weight a b); intros H; auto with datatypes. intro c; simpl; intros [H1 | H1]; subst. left; apply weight_exact; auto. right; apply (Rec l2 c); auto. Qed.
imports: List Permutation UList