proposition: Lemma included_bl {A eq_A} (bl : forall x y : A, eq_A x y = true -> x = y) ls1 ls2 (H : included eq_A ls1 ls2 = true) : incl ls1 ls2.
proof: Proof. unfold included, incl in *. induction ls1; simpl in *; trivial; try tauto. apply Bool.andb_true_iff in H. destruct H as [H0 H1]. specialize (IHls1 H1). intros x [H'|H']; eauto; subst. eapply list_in_bl; eassumption. Defined.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality