proposition: Lemma incl_ok : forall l l', incl l l' = true <-> l [= l'.
proof: Proof. induction l; simpl; intros; auto. intuition. apply incl_nil. split; intro. destruct (andb_elim H). rewrite mem_ok in H0. rewrite IHl in H1. intuition. destruct (incl_cons_l H). rewrite <- mem_ok in H0. rewrite <- IHl in H1. rewrite H0, H1. refl. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)