proposition: Lemma distinct_aux_spec : forall l acc, distinct_aux acc l = true <-> acc = true /\ (forall i j, In2 i j l -> eq i j = false).
proof: Proof. induction l as [ |t q IHq]; simpl. intro acc; split. intro H; split; auto with smtcoq_in2; intros i j H1; inversion H1. intros [H _]; auto with smtcoq_in2. intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec; split. intros [[H1 H2] H3]; split; auto with smtcoq_in2; intros i j H; inversion H; auto with smtcoq_in2. intros [H1 H2]; repeat split; auto with smtcoq_in2. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz