proposition: Lemma equality_from_membership : forall (x y : E) (l : list E), In y l -> ~ In x l -> x <> y.
proof: Proof. simple induction l. simpl in |- *; intuition. intros a l' H. simpl in |- *. case (eq_E_dec a y). intro e. rewrite e. intro H0. intuition. intros n H0 H1. apply H. auto. intuition. intuition. Qed.
imports: List bibli