proposition: Theorem rm_olist_strong: forall a l1 l2, olist (a :: l2) -> olist (a :: rm l1 l2).
proof: Proof. intros a l1; generalize a; elim l1; simpl; auto; clear a l1. intros a l1 Rec c l2; generalize c; elim l2; simpl; auto; clear c l2. intros b l2 Rec1 c H. case_eq (weight a b); intros H1; auto. apply Rec; 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