From 8274f79967e22f72947de4d5130fd661860ee3f9 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 08:51:45 +0000
Subject: [PATCH] Fix proof after reorienting statement

---
 src/list/src/numposrepScript.sml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index 86277ec52f..2b5d8bcff3 100644
--- 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[]