Slightly improved proof of has_hnf_iff_LAM

binghe · Oct 4, 2023 · 8649040 · 8649040
1 parent edaa993
commit 8649040
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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]