encode (x = y => fx = fy), fixing previous false counterexample

This pull request encodes knowledge about the relation between arguments and results of functions, i.e. (`x` ... = `y` ...) implies (`fx⋯` = `fy⋯`), where `fx⋯` is the symbol resulting from (`f` `x` ...)