proposition: Lemma list_beq_eqlistA_iff {A eq_A} {x y : list A} : list_beq eq_A x y = true <-> SetoidList.eqlistA eq_A x y.
proof: Proof. split; intro H. { generalize dependent y; induction x as [|x xs IHxs]; simpl; intros [|??]; simpl; intro H; try discriminate; constructor. { apply Bool.andb_true_iff in H; apply H. } { apply Bool.andb_true_iff in H. destruct H. eauto with nocore. } } { induction H; simpl; try reflexivity. apply Bool.andb_true_iff; split; assumption. } 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