proposition: Theorem in_inv_dec: forall (a b : A) l, In a (cons b l) -> a = b \/ ~ a = b /\ In a l.
proof: Proof. intros a b l H; case (eqA_dec a b); auto; intros H1. right; split; auto; inversion H; auto. case H1; auto. Qed.
imports: List Arith Permutation ListSet