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