splitlist : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
splitlist d (f(x1,f(x2,f(...f(xn,y)))))
([x1; ... ; xn],y)
# splitlist dest_forall `!x y z. x + y = z`;; val it : term list * term = ([`x`; `y`; `z`], `x + y = z`)