From 38698d2c22419daf00c5f4549162ab3fa09a7f70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 15 Jul 2025 18:12:13 +0200
Subject: [PATCH] detail

---
 Z.lp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Z.lp b/Z.lp
index e8ffc36..1443d6a 100644
--- a/Z.lp
+++ b/Z.lp
@@ -557,10 +557,10 @@ begin
    { assume y h H; refine H }
    { assume x;
      induction
-      { assume h1 h2; refine λ x, x;   }
-      { assume y h h'; refine λ x, x }
-      { simplify; assume y h f; apply ⊥ₑ; refine f ⊤ᵢ } }
-  { assume x y f h; apply ⊥ₑ; refine f ⊤ᵢ }
+      { assume h1 h2; refine h1 }
+      { assume y h h' i; refine i }
+      { assume y h f i; refine f ⊤ᵢ } }
+  { assume x y f h i; refine f ⊤ᵢ }
 end;
 
 symbol <_compat_≤ x y : π (Z0 < x ⇒ Z0 ≤ y ⇒ Z0 < x + y) ≔