diff --git a/hol4/transScript.sml b/hol4/transScript.sml
index ceeb7b6b7bdd211ccff5c3c46dcc9ed27f4ca2b5..82d350a44995c2a75b59086360823839f72deaa9 100644
--- a/hol4/transScript.sml
+++ b/hol4/transScript.sml
@@ -1,4 +1,3 @@
-
 open preamble
 open simpLib realTheory realLib RealArith stringTheory
 
@@ -190,7 +189,7 @@ val precond_validErrorbound_true = prove (``
       \\ first_x_assum irule
       \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
       \\ rw_asm_star `absenv _ = _`
-      \\ Cases_on `absenv x12`
+      \\ Cases_on `absenv x15`
       \\ fs [])
   \\ conj_tac
   >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
@@ -240,6 +239,10 @@ val precond_validErrorbound_true = prove (``
         \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
         \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
         \\ REAL_ASM_ARITH_TAC))
+  \\ conj_tac
+  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
+      \\ rpt conj_tac \\ first_x_assum match_mp_tac
+          \\ fs [Once validIntervalbounds_def])
   \\ rpt strip_tac
   \\ rveq
   \\ fs[]