Como podemos provar que se para todas as entradas fe gretornar a mesma saída, então as duas funções são equivalentes?
lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g
Eu diria que isso é um axioma, mas não funciona. A extensionalidade da função não é verdadeira em Dafny?