「同じ」とは何か？

Print eq.
(* ===> Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x *)

eq_reflは引数を持たないコンストラクタ。
eq_reflを実行すると、なんらかの型Aの値xを取って、 eq x x (x = x)という命題型の値(つまり証明or根拠)を返す関数？を返す？

Goal 1 + 0 = 1.
Proof.
reflexivity.
Show Proof. (* ===> eq_refl 
なんで、eq_refl 1 ではないのか？
*)
Qed.

右辺と左辺が同じ等式で終る証明は、両辺の値がなんであれ、eq_reflの呼出し一つで事足りるようだ。

何か不思議な気がしていたけど、こうして書いてみると、それしかありえない気もする。

命題なのか、その命題の証明なのか？やっぱり良くわかってなかったわ。自分。