Make a small summary file

[benediktahrens]

The summary file should state the main theorems outside any section, that is, with all the hypotheses inside the statement of the theorem.

For its proof, it can apply the theorem proved in another file.

[benediktahrens]

Addendum: the file could look similar to this one: https://github.com/UniMath/UniMath/blob/master/UniMath/SubstitutionSystems/SubstitutionSystems_Summary.v

[benediktahrens]

The summary file should also contain a theorem about representability of equations with target Theta^(n).