Add a transformation "extensionality" to help with proofs of equality.
Adding meta extensionality function byte'int to the following file makes Alt-Ergo go from 22 to 16 steps:
use mach.int.Byte
let foo (x : byte) ensures { result = x } = x + 0
Adding meta extensionality predicate Seq.(==) to the following file makes Alt-Ergo go from timeout to instant:
use int.Int
use seq.Seq
let foo () =
let s1 = create 5 (fun i -> i) in
let s2 = create 5 (fun i -> i + 0) in
assert { s1 = s2 }