Instantiated Facts

Created by: SimonGuilloud

Facts in proofs can now be InstantiatedFacts. They can be used in premisces of proof step and are automatically computed from the base fact.

Removed use of projection types in multiple places, as it is apparently bad practice. More changes to accomodate the two previous ones. Deconstruct Unordered Pair theorem went down to 3 lines, from the initial 120.