proposition: Theorem merge_inv: forall a l1 l2, In a (merge l1 l2) -> In a l1 \/ In a l2.
proof: Proof. intros a l1; elim l1; simpl; auto; clear l1. intros b l1 Rec l2; elim l2; simpl; auto; clear l2. intros [H | H]; auto. case (Rec nil); auto. intros c l2 Rec1; case (weight b c); simpl; intros [H | H]; subst; auto. case (Rec (c :: l2)); auto. case (Rec l2); auto. case Rec1; auto. Qed.
imports: List Permutation UList