match goal with当在用户定义的策略中进行模式匹配（with ）时，我们可以使用?x绑定一个 Gallina 术语，以便稍后我们可以引用它。我们可以在一个子句中使用多个这样的标识符 ( ... ?x ... ?y ...)，或者我们甚至可以使用相同的标识符 ( ... ?x ... ?x ...) 来指示为了使子句匹配，相同的 Gallina 术语必须出现在这两个位置。在某种程度上，这限制了与“相同”要求的可能匹配。这很方便，但也能够提出“不同”的要求会更方便（原文如此）。有没有办法编写一个匹配子句的形式... ?x ... ?y ...，我们要求受约束的术语?x是?y可区分的？
通过可区分我不一定意味着不相等，而只是不同（它们的名称[或表示]不重合）。例如，假设我有两个术语a,b:C。在我们可以证明命题的意义上，这两个术语可能相等a = b，但这与我的目的无关。彼此的区别和区别在于它们的名称不同a。b
那么，我可以通过提出两个元变量?x并且?y必须绑定不同的术语的要求来进行模式匹配吗？
把它放在某种上下文中，假设我们已经定义了对、投影，并且 letR是一些（适当类型的）二元关系。假设我在我的假设中以某种方式结束了以下两个。
H : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a
我希望能够在我的策略中编写一个匹配子句，它只会匹配H而不匹配H'。有什么诀窍吗？
如果没有办法只匹配H，那么也许我可以匹配两者，我绑定a到?x和c（或再次a）到?y。但是，在匹配子句的右侧，我想执行一些“它们不同吗？ ”检查xandy并做idtac，以防两者在字面上绑定相同的术语。