From 86490403ae1d5334a4b0b064789f264bf73b488f Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Wed, 4 Oct 2023 16:50:41 +1100
Subject: [PATCH] Slightly improved proof of has_hnf_iff_LAM

---
 examples/lambda/barendregt/standardisationScript.sml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml
index 2c3dd7123a..160de045bb 100644
--- a/examples/lambda/barendregt/standardisationScript.sml
+++ b/examples/lambda/barendregt/standardisationScript.sml
@@ -2171,7 +2171,6 @@ Proof
  >> rpt STRIP_TAC
  >- (Q.EXISTS_TAC ‘LAM x N’ \\
      CONJ_TAC >- PROVE_TAC [lameq_rules] \\
-    ‘?vs args y. N = LAMl vs (VAR y @* args)’ by METIS_TAC [hnf_cases] \\
      rw [hnf_cases])
  (* stage work *)
  >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR]