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