proposition: Lemma list_in_bl_false {A eq_A} (A_lb : forall x y : A, x = y -> eq_A x y = true) {a ls} : list_bin eq_A a ls = false -> ~List.In a ls.
proof: Proof. intros H H'; eapply list_in_lb in H'; [ | eauto ]; congruence. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common