coq - 标准库中 inl 和 inr 的单射性

Question

在 Coq 标准库中我可以在哪里找到一个引理，指出 inl和inr是注入(inject)吗？即forall (A B : Type)(x y : A), inl B x = inl B y -> x = y ，对于右边的情况也类似。我自己证明这一点没有问题，但这些似乎是非常有用和重要的引理，我必须想象它们已经在标准库中的某个地方。

Answer 1

由于所有归纳类型的构造函数都是单射的，所以定义所有这些引理将是相当麻烦的。可以说，它们可以像定义归纳原理一样自动定义，但是，它们可以从中导出。

无论如何，如果您需要引理是在不同的证明中进行表达，您应该了解策略 injection ，它会为您检索所有必要的等式。