coq - Require Import coq ライブラリの後の bool と Datatypes.bool の混同

Question

2

私はソフトウェア基盤を調べていて、エラーに遭遇しました。( https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html )

From Coq Require Import Arith.Arith.

From Coq Require Import Bool.Bool.

Require Export Coq.Strings.String.

From Coq Require Import Logic.FunctionalExtensionality.

From Coq Require Import Lists.List.

Import ListNotations.

証明の例:

Lemma eqb_stringP : forall x y : string,
    reflect (x = y) (eqb_string x y).

エラー: 環境内 x : string y : string 用語 "eqb_string x y" の型は "bool" ですが、型は "Datatypes.bool" であると予想されます。

続行する方法に関するヒントはありますか？