proposition: Theorem insert_in: forall a l, In a (insert a l).
proof: Proof. intros a l; elim l; simpl; auto. intros b l1 H; case_eq (weight a b); auto with datatypes. intros H1; rewrite weight_exact with (1 := H1); auto with datatypes. Qed.
imports: List Permutation UList