proposition: Theorem insert_inv: forall a b l, In a (insert b l) -> a = b \/ In a l.
proof: Proof. intros a b l; elim l; simpl; auto with datatypes. intuition. intros c l1 H; case_eq (weight b c); simpl; auto with datatypes. intuition. intuition. Qed.
imports: List Permutation UList