Generate rewrite relation (#4745)

Closes #4728

Generates an inductive type `Rewrites : GeneratedTopCell ->
GeneratedTopCell -> Prop` where each constructor (except for the first
one which expresses transitivity) encodes a K rewrite rule.

Each constructor has the following signature:
* An implicit binder for each free variable.
* An explicit binder for each function application which expresses
definedness of the function over the arguments.
* An explicit binder for the requires clause.
* The type `Rewrites <lhs> <rhs>`.

pyk/src/pyk/k2lean4/Prelude.lean

@@ -20,7 +20,7 @@ These theorems should be provable directly from the function rules and the seman
  -/
 
 -- Basic K types
-abbrev SortBool         : Type := Int
+abbrev SortBool         : Type := Bool
 abbrev SortBytes        : Type := ByteArray
 abbrev SortId           : Type := String
 abbrev SortInt          : Type := Int