proposition: Lemma mem_ok x : forall l, mem x l = true <-> In x l.
proof: Proof. induction l; simpl; intros; auto. intuition. split; intro. destruct (orb_true_elim H). rewrite beq_ok in e. subst. auto. intuition. destruct H. subst. rewrite (beq_refl beq_ok). refl. intuition. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)