使用 ssreflect，我爱上了它积极管理进出目标的活页夹的风格。但是，我在从其文档中搜索我想要的内容时遇到了问题。
特别是，我找不到该策略的 ssreflectinversion策略。
我知道我可以很好地使用inversion战术。然而，它在使用活页夹时遵循了传统的 coq 风格，我很难为每个分支指定正确的名称，因为它从多目标视图中“隐藏”了。同时，ssreflect 策略总是将绑定器释放到目标中，因此我可以将名称绑定到类似的move。
例如，通过在 上应用反转Forall2 R l m，我得到
x0: A
y0: B
l0: list A
l': list B
H3: R x y
H5: Forall2 R l m
H0: x0 = x
H1: l0 = l
H2: y0 = y
H4: l' = m
这是我不喜欢的名称，并且跟踪和指定这些名称会很痛苦，因为绑定隐藏在第二个分支后面（第一个分支只是l = m = []）。
如果我想以 ssreflect 风格反转归纳类型，我可以使用什么？可以elim用于某种反转吗？