proposition: Theorem add_incl_r: forall l1 l2, incl l2 (add 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. Qed.
imports: List Permutation UList