proposition: Lemma Inclb_ok : forall l1 l2, Inclb l1 l2 = true <-> l1 [= l2.
proof: Proof. intros. induction l2. unfold Inclb. simpl. case l1. simpl; split; auto. intro. refl. intros. simpl; split; intro. discr. rewrite incl_nil_elim in H. discr. split; unfold Inclb; simpl; rewrite forallb_forall; intro. intros x Hx. gen (H _ Hx). case (eq_dec x a); intros. rewrite e; apply in_eq. apply in_cons. apply Inb_true; auto. intros. case (eq_dec x a); auto; intros. destruct (in_inv (H _ H0)); auto. apply Inb_intro; auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)