Restricted function theorems

Description

This PR proves several theorems regarding restricted functions. Notably, it proves the relation domain of a restricted function

relationDomain(restrictedFunction(f, x)) === setIntersection(x, relationDomain(f))

as well as a cancellation theorem:

restrictedFunction(f, relationDomain(f)) === f

that is useful for group theory.

It also contains several tactics imported from the Work-in-Progress on Group Theory (#151), as well as first-order logic lemmas for proving the theorem.

Note that since Definition tactic uses Tautology, I placed the tactics in the main submodule instead of SimpleDeducedSteps.