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.
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.