我们如何证明如果对于所有输入，f并且g返回相同的输出，那么这两个函数是等价的？
lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g
我认为这是一个公理，但它不起作用。Dafny 中的函数外延性不成立吗？
AskOverflow.Dev
