标准库中inl和inr的注入性

Question

在Coq标准库中我可以找到一个说明inl并inr注射的引理吗？也就是说forall (A B : Type)(x y : A), inl B x = inl B y -> x = y,并且类似于右手情况.我自己没有问题证明这一点,但这些似乎是非常有用和重要的引理,我必须想象它们已经在某个地方的标准库中了.

Answer 1

由于归纳类型的所有构造函数都是单射的,因此定义所有这些引理将是非常麻烦的.可以说,它们可以按照定义归纳原则的方式自动定义,但是,它们可以从它们中获得.

无论如何,如果你对引理的需要是用不同的证据来表达,你应该知道战术注入,它会为你找回所有必要的平等.