proposition: Lemma list_lbA {A eq_A} {R : relation A} (A_lb : forall x y : A, R x y -> eq_A x y = true) {x y : list A} : SetoidList.eqlistA R x y -> list_beq eq_A x y = true.
proof: Proof. generalize dependent y; induction x as [|x xs IHxs]; simpl; intros [|??]; simpl; intro H; try solve [ reflexivity | discriminate ]; inversion H; subst; clear H. apply Bool.andb_true_iff. split; eauto with nocore. 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