Support for type variables

[Mallku2]

This PR introduces support for Eunoia's Type variables:

• It correctly compiles the examples contained in our benchmark set, except for the 2 rules that make use of the operator /_total, which still needs to be supported. Note that some lemmas generated contain sorry.
• While the benchmark set is rather simpler, in the sense that every different Type variable referred in a single rule always ends up referring to the same type, it is still possible to test our tool with examples where the Type variables might refer to different types, and the compilation succeeds in dealing with that situation. For example, for the rule:

(declare-rule test ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1))
  :args (t1 s1)
  :conclusion (= t1 t1)
)

the generated lemmas is:

lemma test:
  fixes s1 :: "'b :: type" and t1 :: "'a :: type"
  shows "t1 = t1"
  apply simp ?
  done

• It was not possible to use the identifier dummy suffixed by the variable name, when generating the schematic type variable that represents a given Eunoia's Type variable. If doing so, the compilation results in errors like the following:

Type unification failed: Variable ?dummyTYPE@T0.0::{} not of sort type

Failed to meet type constraint:

Term:  All :: (??'a::type ⇒ bool) ⇒ bool
Type:  (?dummyTYPE@T0.0::{} ⇒ bool) ⇒ bool

Co-authored-by: @Lachnitt