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