Wrap types (if needed) before comparing or asserting.

[DikieDick]

The goal of this PR is to add an utility function (called 'correct_type_by_wrapping') that fixes some issues regarding the types of (namely) boolean statements when comparing or asserting.

Example:

Either (x = y) or (x != y).

Would not work before as the x != y term has type bool and needed to be wrapped in is_true.

This also causes problems when comparing the type of the statement x != y as done in Since, since the type of x != y is not 'Type', 'Set' or 'Prop'.

I have created the utility function correct_type_by_wrapping that

1. Adds the 'is_true' wrapping to booleans.
2. Leaves 'Prop', 'Type' and 'Set' unchanged.
3. Throws an error if a statement with type other than 'bool', 'Prop', 'Type' or 'Set' is encountered.

Where necessary this function has been added to the tactics in the library.

Changes:

• Added theories/Util/TypeCorrector.v
• Added tests/util/TypeCorrector.v
• Added calls to correct_type_by_wrapping from TypeConstructor to Waterproof tactics where needed.

[DikieDick]

Finally, could you please check locally if the compilation with this new branch has slowed down. I compiled twice and once was very slow, the second time was much faster.

I have not noticed any slowdowns in my development. Running hyperfine to test on 10 compilation runs (dune clean; dune build) gave the following:	Branch	Mean [s]	Min [s]	Max [s]	Relative
main	38.648 ± 1.035	37.676	41.229	1.01 ± 0.03
TypeCorrector	38.347 ± 0.599	37.398	39.339	1.00

Command: hyperfine --warmup 3 "git switch main; dune clean; dune build" "git switch TypeCorrector; dune clean; dune build" --export-markdown "../main.md"