Fix proof after reorienting statement

HOL-Theorem-Prover · Dec 18, 2024 · 8274f79 · 8274f79
1 parent 4d1168d
commit 8274f79
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
@@ -446,7 +446,6 @@ Proof
   Induct
   \\ rw[l2n_def]
   \\ fs[EXP, ADD1]
-  \\ first_x_assum(CHANGED_TAC o SUBST1_TAC o SYM)
   \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
   \\ Q.SPECL_THEN[`ls`,`2`]mp_tac l2n_lt
   \\ simp[]