proposition: Theorem rm_in: forall (a: A) l1 l2, olist l1 -> olist l2 -> ~ In a l1 -> In a l2 -> In a (rm l1 l2).
proof: Proof. intros a l1; generalize a; elim l1; simpl; auto; clear a l1. intros b l1 Rec a l2 H1 H2 H3 H4. generalize H2 H4; elim l2; simpl; auto; clear l2 H2 H4. assert (O1: olist l1); try apply olist_inv with (1 := H1). intros c l3 Rec1 H4 [H5 | H5]; subst. case_eq (weight b a); auto with datatypes; intros H5. case H3; rewrite weight_exact with (1 := H5); auto. assert (O2: olist l3); try apply olist_inv with (1 := H4). case_eq (weight b c); auto with datatypes; intros H6. Qed.
imports: List Permutation UList