Untitled

Theorem eqb_list_true_iff :
  forall A (eqb : A -> A -> bool),
    (forall a b, eqb a b = true <-> a = b) ->
    forall xs ys, eqb_list eqb xs ys = true <-> xs = ys.
Proof.
  intros A eqb Heq.
  induction xs as [|x xs' IHxs'].
  - destruct ys as [|y ys'].
    + simpl. split; reflexivity.
    + simpl. split; intros Hoops; inversion Hoops.
  - destruct ys as [|y ys'].
    + simpl. split; intros Hoops; inversion Hoops.
    + simpl.
      destruct (eqb x y) eqn:Hxy.
      * rewrite Heq in Hxy. subst y. split.
        -- intros Hxys. f_equal. rewrite <- IHxs'. assumption.
        -- intros Hxys. rewrite IHxs'. inversion Hxys. reflexivity.
      * assert (Hne : x <> y). { intros Hoops. rewrite <- Heq, Hxy in Hoops. inversion Hoops. }
        split.
        -- intros Hoops. inversion Hoops.
        -- intros Hxys. inversion Hxys. contradiction.
Qed.
```