pure_prove_recursive_function_exists : term -> thm
?f. (f [] = a) /\ (!h t. CONS h t = k[f,h,t])
?f. (!n. f(2 * n) = a[f,n]) /\ (!n. f(2 * n + 1) = b[f,n])
?f. (!n. f(n + 1) = 1) /\ (!n. f(n + 2) = 2)
# pure_prove_recursive_function_exists `?fib. fib 0 = 1 /\ fib 1 = 1 /\ !n. fib(n + 2) = fib(n) + fib(n + 1)`;; val it : thm = ?(<<). WF (<<) /\ (!n. T ==> n << n + 2) /\ (!n. T ==> n + 1 << n + 2) |- ?fib. fib 0 = 1 /\ fib 1 = 1 /\ (!n. fib (n + 2) = fib n + fib (n + 1))