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
-