假设我们正在使用一对类型('a × 'a)并为它定义一个fun模式匹配。
fun test :: "('a × 'a) ⇒ 'a ⇒ bool" where "test (a,b) c = True"
如果我现在有一个a_btype 变量，('a × 'a)我如何(a,b)在应用样式证明中将其替换为它的对表示。例如，显示以下引理的最佳方式是什么？我该如何test a_b c替换test (a,b) c？
lemma "test a_b c = True"
这是否也适用于假设中的对？
lemma "¬ test a_b c ⟹ flying_pigs"