proposition: Lemma distinct_aux2_spec_neg : forall ref l acc, distinct_aux2 acc ref l = false <-> acc = false \/ (exists i, In i l /\ eq ref i = true).
proof: Proof. intro ref; induction l as [ |t q IHq]; simpl. intro acc; split; auto; intros [H|[i [H _]]]; auto; elim H. intro acc; rewrite (IHq (acc && negb (eq ref t))); rewrite andb_false_iff;split. intros [[H|H]|[i [H1 H2]]]; auto. right; exists t; split; auto; generalize H; case (eq ref t); auto. right; exists i; split; auto. intros [H|[i [[H1|H1] H2]]]; auto. subst t; left; right; generalize H2; case (eq ref i); auto. right; exists i; auto. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz