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