Automatic proofs or model checking in an extremely simplified functional language
The ACL2 system includes all of the features of your language, and supports impressive automated theorem proving about program in that language.

In ACL2, you would write the theorem you describe as:

(defthm f-g-equal (equal (f x) (g x)))


having previously defined f and g.