diff --git a/.github/workflows/pvs_prelude.yml b/.github/workflows/pvs_prelude.yml
index 7733581eb935556f20edcf18f41a01b6992d7930..f9ce15ac4d0416597b3a342acd090ae1d351103b 100644
--- a/.github/workflows/pvs_prelude.yml
+++ b/.github/workflows/pvs_prelude.yml
@@ -23,5 +23,4 @@ jobs:
       run: |
         eval $(cd "${HOME}"/lambdapi; opam env)
         cd pvs-translation-tools/prelude || exit 1
-        patch theories theories.patch # Apply patch for typechecking
         bmake
diff --git a/pvs-translation-tools/prelude/theories b/pvs-translation-tools/prelude/theories
index e28b829f7b82279d2b3db7ee37390838bd9a2a90..319511d04e4eec4f43fb2ef2327ed65d59ca07da 100644
--- a/pvs-translation-tools/prelude/theories
+++ b/pvs-translation-tools/prelude/theories
@@ -71,17 +71,17 @@ floor_ceil
 euclidean_division
 divides
 modulo_arithmetic
-subrange_inductions
+-subrange_inductions # FIXME: Ill formed application (term is not typed in PVS)
 bounded_int_inductions
 bounded_nat_inductions
-subrange_type
-int_types
-nat_types
+-subrange_type # Overloading on dependent types needed
+-int_types # Overloading on dependent types
+-nat_types # Overloading on dependent types
 nat_fun_props
-finite_sets
-restrict_set_props
-extend_set_props
-function_image_aux
+-finite_sets # Depends on nat_types
+-restrict_set_props # Depends on finite_sets
+-extend_set_props # Depends on finite_sets
+-function_image_aux # Depends on finite_sets
 -function_iterate # Recursive function definition
 sequences
 seq_functions
@@ -94,8 +94,8 @@ seq_functions
 -lex4 # Depends on ordinals
 -list # Is a datatype
 -list_props # Recursive function
-map_props
-more_map_props
+-map_props # Depends on list
+-more_map_props # Must depend on map_props or list
 -filters # Recursive functions
 -list2finseq # Depends on list
 -list2set # Recursive functions, depends on list
@@ -105,16 +105,16 @@ more_map_props
 -lift # Is a datatype
 -union # Datatype
 mucalculus
-ctlops
-fairctlops
+-ctlops # Seem to mess with K_conversion
+-fairctlops # Mess with K_conversion
 -Fairctlops # Recursive functions
-bit
-bv
+-bit # FIXME: subtyping failure
+-bv # Depedns on bit
 -exp2 # Recursive functions
-bv_concat_def
-bv_bitwise
+-bv_concat_def # depends on bit
+-bv_bitwise # depedns on bit
 -bv_nat # Recursive
-empty_bv
+-empty_bv # Depends on bit
 -bv_caret # Dependent tuple (I think)
 mod
 -bv_arith_nat_defs # May depend on bv_caret
@@ -126,11 +126,11 @@ mod
 -finite_sets_of_sets # Recursive functions
 EquivalenceClosure
 QuotientDefinition
-KernelDefinition
-QuotientKernelProperties
-QuotientSubDefinition
-QuotientExtensionProperties
-QuotientDistributive
-QuotientIteration
+-KernelDefinition # FIXME: Unification failure
+-QuotientKernelProperties # Depeds on KernelDefinition
+-QuotientSubDefinition # depends on QuotientSubDefinition
+-QuotientExtensionProperties # depends on KernelDefinition
+-QuotientDistributive # Depends on previous theories
+-QuotientIteration # Depends on previous theories
 -PartialFunctionDefinitions # Contains a record
 -PartialFunctionComposition # Depends on previous thy
diff --git a/pvs-translation-tools/prelude/theories.patch b/pvs-translation-tools/prelude/theories.patch
deleted file mode 100644
index 76a24b7192e3e5a7c39496127aaa3330207d6b40..0000000000000000000000000000000000000000
--- a/pvs-translation-tools/prelude/theories.patch
+++ /dev/null
@@ -1,95 +0,0 @@
-diff --git a/translations/prelude/theories b/translations/prelude/theories
-index f239adab..f38a6056 100644
---- a/translations/prelude/theories
-+++ b/translations/prelude/theories
-@@ -65,23 +65,23 @@ real_props
- extra_real_props
- extra_tegies
- rational_props
--integer_props
-+-integer_props # FIXME
- floor_ceil
- -exponentiation # Contains a recursive function definition
- euclidean_division
--divides
--modulo_arithmetic
--subrange_inductions
-+-divides # FIXME: Last declaration fails
-+-modulo_arithmetic # Very long to typecheck
-+-subrange_inductions # FIXME: Ill formed application (term is not typed in PVS)
- bounded_int_inductions
- bounded_nat_inductions
--subrange_type
--int_types
--nat_types
-+-subrange_type # Overloading on dependent types needed
-+-int_types # Overloading on dependent types
-+-nat_types # Overloading on dependent types
- nat_fun_props
--finite_sets
--restrict_set_props
--extend_set_props
--function_image_aux
-+-finite_sets # Depends on nat_types
-+-restrict_set_props # Depends on finite_sets
-+-extend_set_props # Depends on finite_sets
-+-function_image_aux # Depends on finite_sets
- -function_iterate # Recursive function definition
- sequences
- seq_functions
-@@ -94,8 +94,8 @@ seq_functions
- -lex4 # Depends on ordinals
- -list # Is a datatype
- -list_props # Recursive function
--map_props
--more_map_props
-+-map_props # Depends on list
-+-more_map_props # Must depend on map_props or list
- -filters # Recursive functions
- -list2finseq # Depends on list
- -list2set # Recursive functions, depends on list
-@@ -105,18 +105,18 @@ more_map_props
- -lift # Is a datatype
- -union # Datatype
- mucalculus
--ctlops
--fairctlops
-+-ctlops # Seem to mess with K_conversion
-+-fairctlops # Mess with K_conversion
- -Fairctlops # Recursive functions
--bit
--bv
-+-bit # FIXME: subtyping failure
-+-bv # Depedns on bit
- -exp2 # Recursive functions
--bv_concat_def
--bv_bitwise
-+-bv_concat_def # depends on bit
-+-bv_bitwise # depedns on bit
- -bv_nat # Recursive
--empty_bv
-+-empty_bv # Depends on bit
- -bv_caret # Dependent tuple (I think)
--mod
-+-mod # Out of memory
- -bv_arith_nat_defs # May depend on bv_caret
- -bv_int_defs # May depend on bv_caret
- -bv_arithmetic_defs # Recursive functions
-@@ -126,11 +126,11 @@ mod
- -finite_sets_of_sets # Recursive functions
- EquivalenceClosure
- QuotientDefinition
--KernelDefinition
--QuotientKernelProperties
--QuotientSubDefinition
--QuotientExtensionProperties
--QuotientDistributive
--QuotientIteration
-+-KernelDefinition # FIXME: Unification failure
-+-QuotientKernelProperties # Depeds on KernelDefinition
-+-QuotientSubDefinition # depends on QuotientSubDefinition
-+-QuotientExtensionProperties # depends on KernelDefinition
-+-QuotientDistributive # Depends on previous theories
-+-QuotientIteration # Depends on previous theories
- -PartialFunctionDefinitions # Contains a record
- -PartialFunctionComposition # Depends on previous thy