proposition: Lemma check_in_spec : forall x l, check_in x l = true <-> In x l.
proof: Proof. intro x; induction l as [ |t q IHq]; simpl. split; intro H; try discriminate; elim H. case_eq (x =? t). rewrite eqb_spec; intro; subst t; split; auto. intro H; rewrite IHq; split; auto; intros [H1|H1]; auto; rewrite H1, eqb_refl in H; discriminate. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms