proposition: Lemma list_inA_bl_false {A eq_A} {a ls} : list_bin eq_A a ls = false -> ~SetoidList.InA (fun x y : A => eq_A y x) a ls.
proof: Proof. intros H H'; apply list_inA_lb in H'; 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