From a8dc1747aa3af771e7fe3cf7f0355d6beff3d70d Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Fri, 26 Sep 2025 09:03:53 +0200 Subject: [PATCH] Fix `language/pure_valueScript.sml` Subset of @nikos-alexandris commit (82b28597c5fc3a5f52fc3857a3886a5d40c7ba51) Co-authored-by: Nikos Alexandris --- language/pure_valueScript.sml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/language/pure_valueScript.sml b/language/pure_valueScript.sml index 9648a435..1620b7ab 100644 --- a/language/pure_valueScript.sml +++ b/language/pure_valueScript.sml @@ -740,8 +740,8 @@ Proof gvs[Constructor_rep_def,EVERY_MAP] >> first_x_assum match_mp_tac >> match_mp_tac (MP_CANON EVERY_MONOTONIC) >> - first_x_assum(irule_at (Pos last)) >> - rw[] + gvs [EVERY_EL] >> rw [] >> + first_x_assum drule >> rw [] QED Definition v_take_def: @@ -832,4 +832,3 @@ Proof gvs[FORALL_AND_THM,MAP_EQ_EVERY2] >> gvs[LIST_REL_EL_EQN] QED -