proposition: Lemma distinct_spec : forall l, distinct l = true <-> (forall i j, In2 i j l -> eq i j = false).
proof: Proof. unfold distinct; intro l; rewrite distinct_aux_spec; split; auto with smtcoq_in2; intros [_ H]; auto with smtcoq_in2. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz