的概念，定義如下：試着去了解索引類型家庭
Inductive eq (A : Type) (x : A) : A → Prop := eq refl : (eq x) x
Parameter a b : A.
當我考慮它的實例eq a b之一，我讀A -> Prop類型的(eq a)。
那麼，我的問題是，(eq a) b如何確定a和b對應於同一個對象的事實？
對我而言，奇怪的是我們沒有關於(eq a)究竟做什麼的信息。
方程式a是一個謂詞，只有當其參數等於b時才被定義（只有居民eq_refl），其中平等意味着「由類型分析者統一」。所以a必須被Coq看作與b相同，否則Eq a b相當於False。
要添加到約翰的回答，人們似乎體會到正規的描述我給這裏的我是怎麼想的索引類型家庭的直覺：
https://stackoverflow.com/a/24601292/553003
我還想補充一點，還有就是區別鍵入(eq a) b（與eq a b相同），以及具有此類型的術語。
例如，您可以定義：
Definition a_weird_type : Type := eq 0 42.
因爲這樣的類型只是沒有證據的聲明。儘管如此，您應該無法定義a_weird_term類型爲a_weird_type，因爲您永遠不會說服系統0和42實際上是相等的。
注意，還有雖然檢查的一點點，所以你不能定義：
Definition a_weirder_type : Type := eq 42 true. (* Coq will reject this *)
因爲eq類型隱含拿它比較元素的類型，類型系統將確保兩種元素都有這種類型：
Check (@eq nat 42 true).
(* ^^^^ this should have type nat *)
Check (@eq bool 42 true).
(* ^^ this should have type bool *)
Check (@eq nat 23 42).
(* fine, but not provable *)