Benchmarks for the CwF and SplTC equivalence

[tvignon]

Some Benchmark for the CwF and SplTC equivalence, that contain mostly the common part of the two structure and some additional constructions :

• The Ty presheaf
• context extension
• pi A
• te A (the universal term of type A)
• term equivalence between display version (one of them is not shown there but it already done in another PR, and could be adapted to make the equivalence with the middle structure)
• q

For all of those benchmark there is 4 different setting :

1. SplTC to CwF with SplTC as the reference one (the one given while the CwF is generated form the SplTC)
2. CwF to SplTC with CwF as the reference one
3. Middle Structure of the equivalence to CwF with the middle structure as the reference one
4. Middle Structure of the equivalence to SplTC with the middle structure as the reference one