proposition: Theorem is_in_correct: forall a l, olist l -> if is_in a l then In a l else ~ In a l.
proof: Proof. intros a l; elim l; simpl; auto. intros b l1 Rec H. assert (F0: olist l1); try (apply olist_inv with (1 := H)). case_eq (weight a b); intros H1; auto. intros [H3 | H3]; subst; auto. rewrite weight_refl in H1; discriminate. generalize (weight_anti_sym b a); rewrite H1. rewrite olist_weight with (l := l1); simpl; intros; auto; discriminate. rewrite weight_exact with (1 := H1); auto. generalize (Rec F0); case (is_in a l1); auto. intros H3 [H4 | H4]; subst; auto. rewrite weight_refl in H1; discriminate. Qed.
imports: List Permutation UList