Introduction rules for builtins

[utkn]

This PR adds the introduction rules for builtins. These reside in Lampe/Hoare/Builtins.lean.

Noteworthy changes:

• Generic STHoarePureBuiltin abbreviation added. Builtins that are defined with newPureBuiltin or newGenericPureBuiltin can use this to simplify the definition of the rule.
• Equality, addition, subtraction, multiplication and modulus builtins are converted to manual proofs. This is done because they are special cases that newPureBuiltin constructors do not work with. As a result, the references to these builtins in Syntax.lean are now correct and work with all possible types.
• Added EqTp and ArithTp types. Those types define the Tps that can be compared with == and can accommodate the infix arithmetic operations +, -, /, * respectively.
• Arithmetic rules are added to the steps tactic. Note that now we may need to show that ArithTp tp and EqTp tp hold (see Lampe.lean).
• Documentation to STHoare.lean added that explains our interpretation of the Hoare triplets.

In the proofs, I took care to not use non-terminal simp or simp_all without an only directive.

[utkn]

The equality and arithmetic builtins were converted back to typed automatic proofs (i.e., using newGenericPureBuiltin and newGenericBuiltin style). Accordingly, the intro rules are now typed, e.g., instead of eq_intro we have fEq_intro, uEq_intro, ... etc.

[kustosz]

Some changes needed but I don't need to re-review