proposition: Lemma beq_list_ok : forall l m, beq_list l m = true <-> l = m.
proof: Proof. induction l; destruct m; simpl; split; intro; try (refl || discr). destruct (andb_elim H). rewrite beq_ok in H0. subst a0. rewrite IHl in H1. subst m. refl. inversion H. subst a0. subst m. apply andb_intro. rewrite beq_ok. refl. rewrite IHl. refl. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)