proposition: Lemma included_lb {A eq_A} (lb : forall x y : A, x = y -> eq_A x y = true) ls1 ls2 (H : incl ls1 ls2) : included eq_A ls1 ls2 = true.
proof: Proof. unfold included, incl in *. induction ls1; simpl in *; trivial. (rewrite IHls1 by intuition eauto); clear IHls1. rewrite Bool.andb_comm; simpl. eapply list_in_lb; eauto. Defined.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality