Software Foundations卷1 injection_ex3习题证明思路求指导（勿给答案）

证明思路引导 #

• 你当前的假设里存在两个和j相关的等式：H3 : y :: l = j和H1 : j = z :: l，可以先通过等式传递性消去变量j，得到新的等式y :: l = z :: l
• 列表的::（cons）构造子具备单射性，对上面得到的列表相等等式使用injection tactic，就能直接拆分出头部元素相等的结论y = z，和你当前的证明目标z = y是等价的

你提到的给等式两边同加:: l的思路本质上是cons构造子单射性的反向应用，不需要额外调用特殊tactic手动补全构造子，直接对列表相等的式子做injection即可得到元素相等的结论。

内容的提问来源于stack exchange，提问作者Felipe Balbi