鉴于这两种类型，
Inductive unit : Set := tt.
Inductive otherUnit : Set := ttt.
Coq 能证明它们是不同的吗unit <> otherUnit？
两者在排序上都是单例类型Set，因此不容易找到Set -> Prop区分它们的类型。例如，这甚至不进行类型检查
Definition singletonTT (A : Set) : Prop := forall x : A, x = tt.
因为tt有 typeunit而不是A.
实际上，Coq 中允许这两种类型相等；也就是说，你既不能证明它们相等或不同，而且假设两者都是一致的。
您不能用 来表达 singletonTT，因为tt正如您所指出的，它仅对unit类型进行类型检查。相反，你需要A不透明地对待；例如，您可以将单例属性表示为A /\ forall (x y:A), x = y。当然，这两种类型都是单例，因此这并不能区分它们。
如果您确实假设Axiom unit_otherUnit : unit = otherUnit，那么您可以singletonTT通过强制转换tt为otherUnit：来表达类似的内容eq_rec _ (fun S => S) tt otherUnit ax = ttt。
当类型具有不同的基数（这意味着它们不是同构）时，您可以使用它们的基数来区分它们并证明类型是不同的。简单的例子包括 False <> True 和 unit <> bool，更复杂的例子是nat <> (nat -> nat)。