proposition: Lemma check_distinct_spec : forall ha diseq, check_distinct ha diseq = true <-> exists A dist, get_atom ha = Atom.Anop (Atom.NO_distinct A) dist /\ check_diseqs A dist diseq = true.
proof: Proof. intros ha diseq; unfold check_distinct; split. case (get_atom ha); try discriminate; intros [A] l H; exists A; exists l; auto. intros [A [dist [H1 H2]]]; rewrite H1; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms