proposition: Theorem rm_olist: forall l1 l2, olist l2 -> olist (rm l1 l2).
proof: Proof. intros l1; elim l1; simpl; auto; clear l1. intros a l1 Rec l2; case l2; simpl; auto; clear l2. intros b l2 H; case_eq (weight a b); intros H1; auto. apply Rec; auto. apply olist_inv with (1 := H); auto. generalize b H H1; elim l2; simpl; auto; clear b l2 H H1. intros b l2 Rec1 c H H1. case_eq (weight a b); intros H2; auto. apply rm_olist_strong; auto. apply rm_olist_strong; auto. apply olist_skip with (1 := H); auto. apply olist_cons; auto. apply olist_weight with (1 := H); auto with datatypes. apply Rec1; auto. apply olist_inv with (1 := H); auto. Qed.
imports: List Permutation UList