From 2db8ec2fa26ac4a4d825b0e25168eaf03c70462a Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 10:10:40 +0200
Subject: [PATCH 01/24] Start porting step-indexing for Transfinite Iris

---
 Iris/Iris/Algebra/StepIndex.lean       | 0
 Iris/Iris/Algebra/StepIndexFinite.lean | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 Iris/Iris/Algebra/StepIndex.lean
 create mode 100644 Iris/Iris/Algebra/StepIndexFinite.lean

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
new file mode 100644
index 000000000..e69de29bb
diff --git a/Iris/Iris/Algebra/StepIndexFinite.lean b/Iris/Iris/Algebra/StepIndexFinite.lean
new file mode 100644
index 000000000..e69de29bb

From 059e3b7a5c5109789b1cb2931c8a56e3ce8f1fc0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 10:42:46 +0200
Subject: [PATCH 02/24] Introduce the type class `SIdx`

---
 Iris/Iris/Algebra.lean                 |  2 ++
 Iris/Iris/Algebra/StepIndex.lean       | 26 ++++++++++++++++++++++++++
 Iris/Iris/Algebra/StepIndexFinite.lean | 12 ++++++++++++
 3 files changed, 40 insertions(+)

diff --git a/Iris/Iris/Algebra.lean b/Iris/Iris/Algebra.lean
index 79d1581e1..713772252 100644
--- a/Iris/Iris/Algebra.lean
+++ b/Iris/Iris/Algebra.lean
@@ -11,6 +11,8 @@ public import Iris.Algebra.LeibnizSet
 public import Iris.Algebra.LocalUpdates
 public import Iris.Algebra.IProp
 public import Iris.Algebra.OFE
+public import Iris.Algebra.StepIndex
+public import Iris.Algebra.StepIndexFinite
 public import Iris.Algebra.UFrac
 public import Iris.Algebra.Updates
 public import Iris.Algebra.UPred
diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index e69de29bb..110e84a8a 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, Alvin Tang
+-/
+module
+
+public meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+namespace Iris
+
+@[rocq_alias sidx]
+class SIdx (I : Type u) extends LT I, LE I, Zero I where
+  succ : I → I
+  lt_trans : ∀ (n m p : I), n < m → m < p → n < p
+  lt_wf : WellFounded ((· < ·) : I → I → Prop)
+  lt_trichotomyT : ∀ n m : I, n < m ⊕' n = m ⊕' m < n
+  le_lteq : ∀ m n : I, n ≤ m ↔ n < m ∨ n = m
+  not_lt_zero : ∀ n : I, ¬n < Zero.zero
+  lt_succ_self : ∀ n : I, n < succ n
+  succ_le_of_lt : ∀ n m : I, n < m → succ n ≤ m
+  weak_case : ∀ n : I, (Σ' m : I, n = succ m) ⊕' ∀ m : I, m < n → succ m < n
+
+#rocq_ignore SIdxMixin "Use the type class SIdx instead"
diff --git a/Iris/Iris/Algebra/StepIndexFinite.lean b/Iris/Iris/Algebra/StepIndexFinite.lean
index e69de29bb..b7e7377fb 100644
--- a/Iris/Iris/Algebra/StepIndexFinite.lean
+++ b/Iris/Iris/Algebra/StepIndexFinite.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, Alvin Tang
+-/
+module
+
+public meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+namespace Iris

From 946c03e127365afce4386fe22f3045ccf070bcb6 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 10:57:42 +0200
Subject: [PATCH 03/24] First theorem for `SIdx`: `nlt_0_r`

---
 Iris/Iris/Algebra/StepIndex.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 110e84a8a..7ab3cbff3 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -24,3 +24,14 @@ class SIdx (I : Type u) extends LT I, LE I, Zero I where
   weak_case : ∀ n : I, (Σ' m : I, n = succ m) ⊕' ∀ m : I, m < n → succ m < n
 
 #rocq_ignore SIdxMixin "Use the type class SIdx instead"
+
+namespace SIdx
+
+open Iris
+
+variable {I : Type u} [inst : SIdx I] {m n p : I}
+
+@[rocq_alias SIdx.nlt_0_r]
+theorem nlt_0_r : ¬n < 0 := inst.not_lt_zero n
+
+end SIdx

From 8debfd2683805940b56abe93d88ee76ff69ebf45 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 11:53:18 +0200
Subject: [PATCH 04/24] More `Std` classes and more `SIdx` theorems

---
 Iris/Iris/Algebra/StepIndex.lean | 82 ++++++++++++++++++++++++++++++--
 Iris/Iris/Std/Classes.lean       | 15 +++++-
 2 files changed, 91 insertions(+), 6 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 7ab3cbff3..d52112b40 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -6,6 +6,7 @@ Authors: Michael Sammler, Alvin Tang
 module
 
 public meta import Iris.Std.RocqPorting
+public import Iris.Std.Classes
 
 @[expose] public section
 
@@ -14,24 +15,95 @@ namespace Iris
 @[rocq_alias sidx]
 class SIdx (I : Type u) extends LT I, LE I, Zero I where
   succ : I → I
-  lt_trans : ∀ (n m p : I), n < m → m < p → n < p
+  lt_trans : ∀ {n m p : I}, n < m → m < p → n < p
   lt_wf : WellFounded ((· < ·) : I → I → Prop)
   lt_trichotomyT : ∀ n m : I, n < m ⊕' n = m ⊕' m < n
-  le_lteq : ∀ m n : I, n ≤ m ↔ n < m ∨ n = m
-  not_lt_zero : ∀ n : I, ¬n < Zero.zero
+  le_lteq : ∀ {m n : I}, n ≤ m ↔ n < m ∨ n = m
+  not_lt_zero : ∀ n : I, ¬n < 0
   lt_succ_self : ∀ n : I, n < succ n
-  succ_le_of_lt : ∀ n m : I, n < m → succ n ≤ m
+  succ_le_of_lt : ∀ {n m : I}, n < m → succ n ≤ m
   weak_case : ∀ n : I, (Σ' m : I, n = succ m) ⊕' ∀ m : I, m < n → succ m < n
 
+/-- The step-indexing successor operator. -/
+scoped prefix:max "succᵢ" => SIdx.succ
+
+class SIdxFinite (I : Type u) [SIdx I] : Prop where
+  finite_index : ∀ n : I, n = 0 ∨ ∃ m, n = succᵢ m
+
 #rocq_ignore SIdxMixin "Use the type class SIdx instead"
 
 namespace SIdx
 
-open Iris
+open Iris Std
 
 variable {I : Type u} [inst : SIdx I] {m n p : I}
 
 @[rocq_alias SIdx.nlt_0_r]
 theorem nlt_0_r : ¬n < 0 := inst.not_lt_zero n
 
+@[rocq_alias SIdx.lt_succ_diag_r]
+theorem lt_succ_diag_r : n < succᵢ n := inst.lt_succ_self n
+
+@[rocq_alias SIdx.le_succ_l_2]
+theorem le_succ_l_2 (h : n < m) : succᵢ n ≤ m := inst.succ_le_of_lt h
+
+@[rocq_alias SIdx.inhabited]
+instance inhabited : Inhabited I where
+  default := 0
+
+instance lt_irrefl : Irreflexive inst.lt where
+  irrefl := by
+    intro n
+    induction n using lt_wf.induction with
+    | x_1 => assumption
+    | h x ih =>
+      apply ih
+      sorry
+
+@[rocq_alias SIdx.lt_strict]
+instance lt_struct : StrictOrder inst.lt where
+  trans := inst.lt_trans
+
+instance le_antisymm : Antisymmetric Eq inst.le where
+  antisymm := sorry
+
+@[rocq_alias SIdx.le_po]
+instance le_po : PartialOrder inst.le where
+  refl := inst.le_lteq.mpr (.inr rfl)
+  trans := sorry
+
+@[rocq_alias SIdx.lt_le_incl]
+theorem lt_le_incl (h : n < m) : n ≤ m := by
+  apply le_lteq.mpr; left; assumption
+
+@[rocq_alias SIdx.le_total]
+theorem le_total : Total inst.le where
+  total := by
+    intro x y
+    sorry
+
+@[rocq_alias SIdx.lt_le_trans]
+theorem lt_le_trans (h1 : n < m) (h2 : m ≤ p) : n < p := by sorry
+
+@[rocq_alias SIdx.le_lt_trans]
+theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by sorry
+
+@[rocq_alias SIdx.le_succ_l]
+theorem le_succ_l : succᵢ n ≤ m ↔ n < m := sorry
+
+@[rocq_alias SIdx.lt_succ_r]
+theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := sorry
+
+@[rocq_alias SIdx.succ_le_mono]
+theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := sorry
+
+@[rocq_alias SIdx.succ_lt_mono]
+theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := sorry
+
+-- instance succ_inj : Function.Injective Eq Eq (fun x => succᵢ x)
+
+theorem le_succ_diag_r : n ≤ succᵢ n := by
+  apply lt_le_incl
+  apply lt_succ_diag_r
+
 end SIdx
diff --git a/Iris/Iris/Std/Classes.lean b/Iris/Iris/Std/Classes.lean
index 3b147de3c..31852df11 100644
--- a/Iris/Iris/Std/Classes.lean
+++ b/Iris/Iris/Std/Classes.lean
@@ -19,11 +19,16 @@ export Top (top)
 
 notation "⊤" => top
 
-/-- Require that a relation `R` on `a` is reflexive. -/
+/-- Require that a relation `R` on `α` is reflexive. -/
 class Reflexive (R : Relation α) where
   refl {x : α} : R x x
 export Reflexive (refl)
 
+/-- Require that a relation `R` on `α` is irreflexive -/
+class Irreflexive (R : Relation α) where
+  irrefl {x : α} : ¬R x x
+export Irreflexive (irrefl)
+
 /-- Require that a relation `R` on `α` is transitive. -/
 class Transitive (R : Relation α) where
   trans {x y z : α} : R x y → R y z → R x z
@@ -32,6 +37,11 @@ export Transitive (trans)
 /-- Require that a relation `R` on `α` is a preorder, i.e. that it is reflexive and transitive. -/
 class Preorder (R : Relation α) extends Reflexive R, Transitive R
 
+/-- Require that a relation `R` on `α` is a strict order, i.e. that it is irreflexive and transitive. -/
+class StrictOrder (R : Relation α) extends Irreflexive R, Transitive R
+
+class Total (R : Relation α) where
+  total {x y : α} : R x y ∨ R y x
 
 /-- Require that a binary function `f` on `α` is idempotent in a relation `R` on `α`. -/
 class Idempotent (R : Relation α) (f : α → α → α) where
@@ -73,6 +83,9 @@ class Antisymmetric (R : Relation α) (S : outParam <| Relation α) where
   antisymm {x y : α} : (left : S x y) → (right : S y x) → R x y
 export Antisymmetric (antisymm)
 
+/-- A partial order is a pre-order with an antisymmetric relation -/
+class PartialOrder (R : Relation α) extends Preorder R, Antisymmetric Eq R
+
 class Disjoint (α : Type u) where
   disjoint : α -> α -> Prop
 export Disjoint (disjoint)

From be0f833e1fae332e505a463b6e25ca3c6149de14 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 12:00:35 +0200
Subject: [PATCH 05/24] More theorem definitions

---
 Iris/Iris/Algebra/StepIndex.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index d52112b40..e2e08facd 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -102,8 +102,30 @@ theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := sorry
 
 -- instance succ_inj : Function.Injective Eq Eq (fun x => succᵢ x)
 
+@[rocq_alias SIdx.le_succ_diag_r]
 theorem le_succ_diag_r : n ≤ succᵢ n := by
   apply lt_le_incl
   apply lt_succ_diag_r
 
+@[rocq_alias SIdx.neq_0_lt_0]
+theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := sorry
+
+@[rocq_alias SIdx.lt_ge_cases]
+theorem lt_ge_cases : n < m ∨ m ≤ n := sorry
+
+@[rocq_alias SIdx.le_gt_cases]
+theorem le_gt_cases : n ≤ m ∨ m < n := sorry
+
+@[rocq_alias SIdx.le_ngt]
+theorem le_ngt : n ≤ m ↔ ¬ m ≤ n := sorry
+
+@[rocq_alias SIdx.lt_nge]
+theorem lt_nge : n < m ↔ ¬ m ≤ n := sorry
+
+@[rocq_alias SIdx.le_neq]
+theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := sorry
+
+@[rocq_alias SIdx.nlt_succ_r]
+theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := sorry
+
 end SIdx

From dabb7e7c3fda4058427b233f3ec41c0eacb6df8d Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 13:34:39 +0200
Subject: [PATCH 06/24] Four more theorems defined

---
 Iris/Iris/Algebra/StepIndex.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index e2e08facd..b7d297a24 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -128,4 +128,16 @@ theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := sorry
 @[rocq_alias SIdx.nlt_succ_r]
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := sorry
 
+@[rocq_alias SIdx.le_0_l]
+theorem le_0_l : 0 ≤ n := sorry
+
+@[rocq_alias SIdx.le_0_r]
+theorem le_0_r : n ≤ 0 ↔ n = 0 := sorry
+
+@[rocq_alias neq_succ_0]
+theorem neq_succ_0 : succᵢ n ≠ 0 := sorry
+
+@[rocq_alias succ_neq]
+theorem succ_neq : n ≠ succᵢ n := sorry
+
 end SIdx

From 60a74ba04102c46f6250e2c33d6a6787571de33b Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 13:45:39 +0200
Subject: [PATCH 07/24] Prove `lt_le_trans`

---
 Iris/Iris/Algebra/StepIndex.lean | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index b7d297a24..d485a841e 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -64,13 +64,21 @@ instance lt_irrefl : Irreflexive inst.lt where
 instance lt_struct : StrictOrder inst.lt where
   trans := inst.lt_trans
 
+instance le_refl : Reflexive inst.le where
+  refl := inst.le_lteq.mpr <| .inr rfl
+
+instance le_trans : Transitive inst.le where
+  trans := by
+    intro x y z hxy hyz
+    sorry
+
 instance le_antisymm : Antisymmetric Eq inst.le where
-  antisymm := sorry
+  antisymm := by
+    intro x y hxy hyx
+    sorry
 
 @[rocq_alias SIdx.le_po]
 instance le_po : PartialOrder inst.le where
-  refl := inst.le_lteq.mpr (.inr rfl)
-  trans := sorry
 
 @[rocq_alias SIdx.lt_le_incl]
 theorem lt_le_incl (h : n < m) : n ≤ m := by
@@ -83,7 +91,10 @@ theorem le_total : Total inst.le where
     sorry
 
 @[rocq_alias SIdx.lt_le_trans]
-theorem lt_le_trans (h1 : n < m) (h2 : m ≤ p) : n < p := by sorry
+theorem lt_le_trans (h1 : n < m) (h2 : m ≤ p) : n < p := by
+  rcases SIdx.le_lteq.mp h2 with (h2 | h2)
+  · exact SIdx.lt_trans h1 h2
+  · subst h2; exact h1
 
 @[rocq_alias SIdx.le_lt_trans]
 theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by sorry

From 2b569f8dd0624e17fbce0ba466456457e0b74566 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 13:46:56 +0200
Subject: [PATCH 08/24] Prove `le_lt_trans`

---
 Iris/Iris/Algebra/StepIndex.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index d485a841e..aaf6ab3c9 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -94,10 +94,13 @@ theorem le_total : Total inst.le where
 theorem lt_le_trans (h1 : n < m) (h2 : m ≤ p) : n < p := by
   rcases SIdx.le_lteq.mp h2 with (h2 | h2)
   · exact SIdx.lt_trans h1 h2
-  · subst h2; exact h1
+  · subst h2; assumption
 
 @[rocq_alias SIdx.le_lt_trans]
-theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by sorry
+theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
+  rcases SIdx.le_lteq.mp h1 with (h1 | h1)
+  · exact SIdx.lt_trans h1 h2
+  · subst h1; assumption
 
 @[rocq_alias SIdx.le_succ_l]
 theorem le_succ_l : succᵢ n ≤ m ↔ n < m := sorry

From 5d88f417e8fb7d894b22ea18226ad114bf694e5f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 13:49:44 +0200
Subject: [PATCH 09/24] Typo fix

---
 Iris/Iris/Algebra/StepIndex.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index aaf6ab3c9..f39cb91a6 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -103,7 +103,10 @@ theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
   · subst h1; assumption
 
 @[rocq_alias SIdx.le_succ_l]
-theorem le_succ_l : succᵢ n ≤ m ↔ n < m := sorry
+theorem le_succ_l : succᵢ n ≤ m ↔ n < m := by
+
+
+
 
 @[rocq_alias SIdx.lt_succ_r]
 theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := sorry
@@ -131,7 +134,7 @@ theorem lt_ge_cases : n < m ∨ m ≤ n := sorry
 theorem le_gt_cases : n ≤ m ∨ m < n := sorry
 
 @[rocq_alias SIdx.le_ngt]
-theorem le_ngt : n ≤ m ↔ ¬ m ≤ n := sorry
+theorem le_ngt : n ≤ m ↔ ¬ m < n := sorry
 
 @[rocq_alias SIdx.lt_nge]
 theorem lt_nge : n < m ↔ ¬ m ≤ n := sorry

From e02680fca631a62247ed4d76041354db2f0fb8f0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 14:08:00 +0200
Subject: [PATCH 10/24] Prove `succ_le_mono`, `succ_lt_mono`

---
 Iris/Iris/Algebra/StepIndex.lean | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index f39cb91a6..b88c42062 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -104,18 +104,24 @@ theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
 
 @[rocq_alias SIdx.le_succ_l]
 theorem le_succ_l : succᵢ n ≤ m ↔ n < m := by
-
-
-
+  constructor <;> intro h
+  · exact lt_le_trans (lt_succ_self n) h
+  · exact le_succ_l_2 h
 
 @[rocq_alias SIdx.lt_succ_r]
-theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := sorry
+theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := by
+  constructor <;> intro h
+  · have b := le_succ_l_2 h
+    sorry
+  · exact le_lt_trans h lt_succ_diag_r
 
 @[rocq_alias SIdx.succ_le_mono]
-theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := sorry
+theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := by
+  rewrite [le_succ_l, lt_succ_r]; rfl
 
 @[rocq_alias SIdx.succ_lt_mono]
-theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := sorry
+theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := by
+  rewrite [lt_succ_r, le_succ_l]; rfl
 
 -- instance succ_inj : Function.Injective Eq Eq (fun x => succᵢ x)
 

From 96c333cc09d0f9e1ec5b5d14200b328a522b8080 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 14:18:32 +0200
Subject: [PATCH 11/24] Prove `le_0_l`, `le_0_r`

---
 Iris/Iris/Algebra/StepIndex.lean | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index b88c42062..0bbd939fa 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -64,8 +64,12 @@ instance lt_irrefl : Irreflexive inst.lt where
 instance lt_struct : StrictOrder inst.lt where
   trans := inst.lt_trans
 
+/-- For the `rfl` tactic. -/
+@[refl]
+theorem le_refl_thm : n ≤ n := inst.le_lteq.mpr <| .inr rfl
+
 instance le_refl : Reflexive inst.le where
-  refl := inst.le_lteq.mpr <| .inr rfl
+  refl := le_refl_thm
 
 instance le_trans : Transitive inst.le where
   trans := by
@@ -131,7 +135,11 @@ theorem le_succ_diag_r : n ≤ succᵢ n := by
   apply lt_succ_diag_r
 
 @[rocq_alias SIdx.neq_0_lt_0]
-theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := sorry
+theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
+  constructor <;> intro h
+  · sorry
+  · have h1 := nlt_0_r (inst := inst) (n := 0)
+    sorry
 
 @[rocq_alias SIdx.lt_ge_cases]
 theorem lt_ge_cases : n < m ∨ m ≤ n := sorry
@@ -152,13 +160,18 @@ theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := sorry
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := sorry
 
 @[rocq_alias SIdx.le_0_l]
-theorem le_0_l : 0 ≤ n := sorry
+theorem le_0_l : 0 ≤ n := le_ngt.mpr nlt_0_r
 
 @[rocq_alias SIdx.le_0_r]
-theorem le_0_r : n ≤ 0 ↔ n = 0 := sorry
+theorem le_0_r : n ≤ 0 ↔ n = 0 := by
+  constructor <;> intro h
+  · apply antisymm
+    · assumption
+    · exact le_0_l
+  · subst h; rfl
 
 @[rocq_alias neq_succ_0]
-theorem neq_succ_0 : succᵢ n ≠ 0 := sorry
+theorem neq_succ_0 : succᵢ n ≠ 0 := neq_0_lt_0.mpr <| lt_succ_r.mpr le_0_l
 
 @[rocq_alias succ_neq]
 theorem succ_neq : n ≠ succᵢ n := sorry

From f436057f9b15f1fc24d83618ff5acc1184a229b8 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 14:34:13 +0200
Subject: [PATCH 12/24] Towards proving more theorems

---
 Iris/Iris/Algebra/StepIndex.lean | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 0bbd939fa..245a59b0a 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -145,19 +145,35 @@ theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
 theorem lt_ge_cases : n < m ∨ m ≤ n := sorry
 
 @[rocq_alias SIdx.le_gt_cases]
-theorem le_gt_cases : n ≤ m ∨ m < n := sorry
+theorem le_gt_cases : n ≤ m ∨ m < n := by
+  rcases lt_ge_cases (m := n) (n := m) with (h | h)
+  · right; assumption
+  · left; assumption
 
 @[rocq_alias SIdx.le_ngt]
-theorem le_ngt : n ≤ m ↔ ¬ m < n := sorry
+theorem le_ngt : n ≤ m ↔ ¬ m < n := by
+  constructor <;> intro h
+  · sorry
+  · rcases lt_ge_cases (m := n) (n := m) with (h1 | h1) <;> trivial
 
 @[rocq_alias SIdx.lt_nge]
-theorem lt_nge : n < m ↔ ¬ m ≤ n := sorry
+theorem lt_nge : n < m ↔ ¬ m ≤ n := by
+  constructor <;> intro h
+  · sorry
+  · rcases lt_ge_cases (m := m) (n := n) with (h1 | h1) <;> trivial
 
 @[rocq_alias SIdx.le_neq]
-theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := sorry
+theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := by
+  constructor <;> intro h
+  · sorry
+  · rcases h with ⟨h1, h2⟩
+    sorry
 
 @[rocq_alias SIdx.nlt_succ_r]
-theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := sorry
+theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := by
+  constructor <;> intro h
+  · sorry
+  · sorry
 
 @[rocq_alias SIdx.le_0_l]
 theorem le_0_l : 0 ≤ n := le_ngt.mpr nlt_0_r

From f5e0f5a738446da4e9c34c93ebf88525f61c56de Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 15:46:16 +0200
Subject: [PATCH 13/24] Prove properties about `le`

---
 Iris/Iris/Algebra/StepIndex.lean | 60 ++++++++++++++++++--------------
 1 file changed, 33 insertions(+), 27 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 245a59b0a..ef6bf2a56 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -51,42 +51,48 @@ theorem le_succ_l_2 (h : n < m) : succᵢ n ≤ m := inst.succ_le_of_lt h
 instance inhabited : Inhabited I where
   default := 0
 
-instance lt_irrefl : Irreflexive inst.lt where
-  irrefl := by
-    intro n
-    induction n using lt_wf.induction with
-    | x_1 => assumption
-    | h x ih =>
-      apply ih
-      sorry
+theorem lt_irrefl (n : I) : ¬n < n := by
+  intro h
+  induction n using inst.lt_wf.induction with
+  | h n ih => apply ih n <;> exact h
+
+theorem lt_asymm (h : n < m) : ¬m < n := by
+  intro h1
+  apply lt_irrefl n
+  exact inst.lt_trans h h1
 
 @[rocq_alias SIdx.lt_strict]
 instance lt_struct : StrictOrder inst.lt where
+  irrefl := by intro n; exact lt_irrefl n
   trans := inst.lt_trans
 
-/-- For the `rfl` tactic. -/
-@[refl]
-theorem le_refl_thm : n ≤ n := inst.le_lteq.mpr <| .inr rfl
-
-instance le_refl : Reflexive inst.le where
-  refl := le_refl_thm
-
-instance le_trans : Transitive inst.le where
-  trans := by
-    intro x y z hxy hyz
-    sorry
+@[rocq_alias SIdx.lt_le_incl]
+theorem lt_le_incl (h : n < m) : n ≤ m := by
+  apply le_lteq.mpr; left; assumption
 
-instance le_antisymm : Antisymmetric Eq inst.le where
-  antisymm := by
-    intro x y hxy hyx
-    sorry
+/-- For the `rfl` tactic. -/
+@[refl, simp]
+theorem le_refl : n ≤ n := inst.le_lteq.mpr <| .inr rfl
+
+theorem le_trans (h1 : n ≤ m) (h2 : m ≤ p) : n ≤ p := by
+  rcases le_lteq.mp h1 with (h1 | rfl)
+  · rcases le_lteq.mp h2 with (h2 | rfl)
+    · exact lt_le_incl <| inst.lt_trans h1 h2
+    · exact lt_le_incl h1
+  · assumption
+
+theorem le_antisymm (h1 : n ≤ m) (h2 : m ≤ n) : m = n := by
+  rcases le_lteq.mp h1 with (h1 | h1)
+  · rcases le_lteq.mp h2 with (h2 | h2)
+    · exact absurd (inst.lt_trans h1 h2) (lt_irrefl n)
+    · exact h2
+  · subst h1; rfl
 
 @[rocq_alias SIdx.le_po]
 instance le_po : PartialOrder inst.le where
-
-@[rocq_alias SIdx.lt_le_incl]
-theorem lt_le_incl (h : n < m) : n ≤ m := by
-  apply le_lteq.mpr; left; assumption
+  refl := le_refl.refl
+  trans := le_trans.trans
+  antisymm := le_antisymm.antisymm
 
 @[rocq_alias SIdx.le_total]
 theorem le_total : Total inst.le where

From 30096c7118e9bbff9da7539f800f2133db6841c8 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 16:00:37 +0200
Subject: [PATCH 14/24] More proofs

---
 Iris/Iris/Algebra/StepIndex.lean | 55 ++++++++++++++++----------------
 1 file changed, 28 insertions(+), 27 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index ef6bf2a56..6278eb24f 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -72,7 +72,7 @@ theorem lt_le_incl (h : n < m) : n ≤ m := by
 
 /-- For the `rfl` tactic. -/
 @[refl, simp]
-theorem le_refl : n ≤ n := inst.le_lteq.mpr <| .inr rfl
+theorem le_refl : n ≤ n := by apply inst.le_lteq.mpr; right; rfl
 
 theorem le_trans (h1 : n ≤ m) (h2 : m ≤ p) : n ≤ p := by
   rcases le_lteq.mp h1 with (h1 | rfl)
@@ -81,35 +81,45 @@ theorem le_trans (h1 : n ≤ m) (h2 : m ≤ p) : n ≤ p := by
     · exact lt_le_incl h1
   · assumption
 
-theorem le_antisymm (h1 : n ≤ m) (h2 : m ≤ n) : m = n := by
-  rcases le_lteq.mp h1 with (h1 | h1)
-  · rcases le_lteq.mp h2 with (h2 | h2)
-    · exact absurd (inst.lt_trans h1 h2) (lt_irrefl n)
-    · exact h2
-  · subst h1; rfl
+theorem le_antisymm (h1 : m ≤ n) (h2 : n ≤ m) : m = n := by
+  rcases le_lteq.mp h2 with (h2 | h2)
+  · rcases le_lteq.mp h1 with (h1 | h1)
+    · exact absurd (inst.lt_trans h2 h1) (lt_irrefl n)
+    · exact h1
+  · subst h2; rfl
 
 @[rocq_alias SIdx.le_po]
 instance le_po : PartialOrder inst.le where
-  refl := le_refl.refl
-  trans := le_trans.trans
-  antisymm := le_antisymm.antisymm
+  refl := le_refl
+  trans := le_trans
+  antisymm := le_antisymm
+
+@[rocq_alias SIdx.lt_ge_cases]
+theorem lt_ge_cases (m n : I) : n < m ∨ m ≤ n := by
+  rcases inst.lt_trichotomyT n m with (h | h | h)
+  · left; exact h
+  · right; apply le_lteq.mpr; right; symm; assumption
+  · right; exact lt_le_incl h
+
+@[rocq_alias SIdx.le_gt_cases]
+theorem le_gt_cases (m n : I) : n ≤ m ∨ m < n := lt_ge_cases n m |>.symm
 
 @[rocq_alias SIdx.le_total]
-theorem le_total : Total inst.le where
-  total := by
-    intro x y
-    sorry
+theorem le_total : n ≤ m ∨ m ≤ n := by
+  rcases lt_ge_cases m n with (h | h)
+  · left; exact lt_le_incl h
+  · right; assumption
 
 @[rocq_alias SIdx.lt_le_trans]
 theorem lt_le_trans (h1 : n < m) (h2 : m ≤ p) : n < p := by
-  rcases SIdx.le_lteq.mp h2 with (h2 | h2)
-  · exact SIdx.lt_trans h1 h2
+  rcases inst.le_lteq.mp h2 with (h2 | h2)
+  · exact inst.lt_trans h1 h2
   · subst h2; assumption
 
 @[rocq_alias SIdx.le_lt_trans]
 theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
-  rcases SIdx.le_lteq.mp h1 with (h1 | h1)
-  · exact SIdx.lt_trans h1 h2
+  rcases inst.le_lteq.mp h1 with (h1 | h1)
+  · exact inst.lt_trans h1 h2
   · subst h1; assumption
 
 @[rocq_alias SIdx.le_succ_l]
@@ -147,15 +157,6 @@ theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
   · have h1 := nlt_0_r (inst := inst) (n := 0)
     sorry
 
-@[rocq_alias SIdx.lt_ge_cases]
-theorem lt_ge_cases : n < m ∨ m ≤ n := sorry
-
-@[rocq_alias SIdx.le_gt_cases]
-theorem le_gt_cases : n ≤ m ∨ m < n := by
-  rcases lt_ge_cases (m := n) (n := m) with (h | h)
-  · right; assumption
-  · left; assumption
-
 @[rocq_alias SIdx.le_ngt]
 theorem le_ngt : n ≤ m ↔ ¬ m < n := by
   constructor <;> intro h

From 904795a41de50d6cca42aad1e636a5323ecd6c3d Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 16:22:43 +0200
Subject: [PATCH 15/24] Even more proofs

---
 Iris/Iris/Algebra/StepIndex.lean | 37 ++++++++++++++++++++------------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 6278eb24f..54925d0e7 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -42,7 +42,7 @@ variable {I : Type u} [inst : SIdx I] {m n p : I}
 theorem nlt_0_r : ¬n < 0 := inst.not_lt_zero n
 
 @[rocq_alias SIdx.lt_succ_diag_r]
-theorem lt_succ_diag_r : n < succᵢ n := inst.lt_succ_self n
+theorem lt_succ_diag_r (n : I) : n < succᵢ n := inst.lt_succ_self n
 
 @[rocq_alias SIdx.le_succ_l_2]
 theorem le_succ_l_2 (h : n < m) : succᵢ n ≤ m := inst.succ_le_of_lt h
@@ -133,7 +133,7 @@ theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := by
   constructor <;> intro h
   · have b := le_succ_l_2 h
     sorry
-  · exact le_lt_trans h lt_succ_diag_r
+  · exact le_lt_trans h <| lt_succ_diag_r m
 
 @[rocq_alias SIdx.succ_le_mono]
 theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := by
@@ -159,28 +159,33 @@ theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
 
 @[rocq_alias SIdx.le_ngt]
 theorem le_ngt : n ≤ m ↔ ¬ m < n := by
-  constructor <;> intro h
-  · sorry
-  · rcases lt_ge_cases (m := n) (n := m) with (h1 | h1) <;> trivial
+  constructor <;> intro h0
+  · intro h1
+    exact lt_irrefl m (lt_le_trans h1 h0)
+  · rcases lt_ge_cases n m <;> trivial
 
 @[rocq_alias SIdx.lt_nge]
 theorem lt_nge : n < m ↔ ¬ m ≤ n := by
-  constructor <;> intro h
-  · sorry
-  · rcases lt_ge_cases (m := m) (n := n) with (h1 | h1) <;> trivial
+  constructor <;> intro h0
+  · intro h1
+    exact lt_irrefl n <| lt_le_trans h0 h1
+  · rcases lt_ge_cases m n <;> trivial
 
 @[rocq_alias SIdx.le_neq]
 theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := by
   constructor <;> intro h
-  · sorry
+  · refine ⟨lt_le_incl h, ?_⟩
+    rintro rfl
+    exact lt_irrefl n h
   · rcases h with ⟨h1, h2⟩
-    sorry
+    apply lt_nge.mpr
+    intro h3
+    apply h2
+    exact le_antisymm h1 h3
 
 @[rocq_alias SIdx.nlt_succ_r]
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := by
-  constructor <;> intro h
-  · sorry
-  · sorry
+  rw [lt_succ_r, lt_nge]
 
 @[rocq_alias SIdx.le_0_l]
 theorem le_0_l : 0 ≤ n := le_ngt.mpr nlt_0_r
@@ -197,6 +202,10 @@ theorem le_0_r : n ≤ 0 ↔ n = 0 := by
 theorem neq_succ_0 : succᵢ n ≠ 0 := neq_0_lt_0.mpr <| lt_succ_r.mpr le_0_l
 
 @[rocq_alias succ_neq]
-theorem succ_neq : n ≠ succᵢ n := sorry
+theorem succ_neq : n ≠ succᵢ n := by
+  intro h
+  have hlt := inst.lt_succ_diag_r n
+  rw [← h] at hlt
+  exact lt_irrefl n hlt
 
 end SIdx

From 1aee575e4fd41002569f0636a14b4dccd81e9d0a Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 16:30:01 +0200
Subject: [PATCH 16/24] Further proofs

---
 Iris/Iris/Algebra/StepIndex.lean | 66 +++++++++++++++++---------------
 1 file changed, 36 insertions(+), 30 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 54925d0e7..2ca10cdbb 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -39,7 +39,7 @@ open Iris Std
 variable {I : Type u} [inst : SIdx I] {m n p : I}
 
 @[rocq_alias SIdx.nlt_0_r]
-theorem nlt_0_r : ¬n < 0 := inst.not_lt_zero n
+theorem nlt_0_r (n : I) : ¬n < 0 := inst.not_lt_zero n
 
 @[rocq_alias SIdx.lt_succ_diag_r]
 theorem lt_succ_diag_r (n : I) : n < succᵢ n := inst.lt_succ_self n
@@ -122,27 +122,6 @@ theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
   · exact inst.lt_trans h1 h2
   · subst h1; assumption
 
-@[rocq_alias SIdx.le_succ_l]
-theorem le_succ_l : succᵢ n ≤ m ↔ n < m := by
-  constructor <;> intro h
-  · exact lt_le_trans (lt_succ_self n) h
-  · exact le_succ_l_2 h
-
-@[rocq_alias SIdx.lt_succ_r]
-theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := by
-  constructor <;> intro h
-  · have b := le_succ_l_2 h
-    sorry
-  · exact le_lt_trans h <| lt_succ_diag_r m
-
-@[rocq_alias SIdx.succ_le_mono]
-theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := by
-  rewrite [le_succ_l, lt_succ_r]; rfl
-
-@[rocq_alias SIdx.succ_lt_mono]
-theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := by
-  rewrite [lt_succ_r, le_succ_l]; rfl
-
 -- instance succ_inj : Function.Injective Eq Eq (fun x => succᵢ x)
 
 @[rocq_alias SIdx.le_succ_diag_r]
@@ -150,13 +129,6 @@ theorem le_succ_diag_r : n ≤ succᵢ n := by
   apply lt_le_incl
   apply lt_succ_diag_r
 
-@[rocq_alias SIdx.neq_0_lt_0]
-theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
-  constructor <;> intro h
-  · sorry
-  · have h1 := nlt_0_r (inst := inst) (n := 0)
-    sorry
-
 @[rocq_alias SIdx.le_ngt]
 theorem le_ngt : n ≤ m ↔ ¬ m < n := by
   constructor <;> intro h0
@@ -183,12 +155,36 @@ theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := by
     apply h2
     exact le_antisymm h1 h3
 
+@[rocq_alias SIdx.le_succ_l]
+theorem le_succ_l : succᵢ n ≤ m ↔ n < m := by
+  constructor <;> intro h
+  · exact lt_le_trans (lt_succ_self n) h
+  · exact le_succ_l_2 h
+
+@[rocq_alias SIdx.lt_succ_r]
+theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := by
+  constructor <;> intro h
+  · refine le_ngt.mpr ?_
+    intro h1
+    apply lt_irrefl n
+    apply lt_le_trans h
+    exact le_succ_l_2 h1
+  · exact le_lt_trans h <| lt_succ_diag_r m
+
+@[rocq_alias SIdx.succ_le_mono]
+theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := by
+  rewrite [le_succ_l, lt_succ_r]; rfl
+
+@[rocq_alias SIdx.succ_lt_mono]
+theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := by
+  rewrite [lt_succ_r, le_succ_l]; rfl
+
 @[rocq_alias SIdx.nlt_succ_r]
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := by
   rw [lt_succ_r, lt_nge]
 
 @[rocq_alias SIdx.le_0_l]
-theorem le_0_l : 0 ≤ n := le_ngt.mpr nlt_0_r
+theorem le_0_l : 0 ≤ n := le_ngt.mpr <| nlt_0_r n
 
 @[rocq_alias SIdx.le_0_r]
 theorem le_0_r : n ≤ 0 ↔ n = 0 := by
@@ -198,6 +194,16 @@ theorem le_0_r : n ≤ 0 ↔ n = 0 := by
     · exact le_0_l
   · subst h; rfl
 
+@[rocq_alias SIdx.neq_0_lt_0]
+theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
+  constructor
+  · intro h
+    rcases lt_ge_cases n 0 with (h1 | h1)
+    · assumption
+    · exact absurd (le_0_r.mp h1) h
+  · rintro h rfl
+    exact inst.nlt_0_r 0 h
+
 @[rocq_alias neq_succ_0]
 theorem neq_succ_0 : succᵢ n ≠ 0 := neq_0_lt_0.mpr <| lt_succ_r.mpr le_0_l
 

From 2ac43a81d0ab7ab26c9e423a1eaf5f25dec9ae62 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 16:32:36 +0200
Subject: [PATCH 17/24] Prove `succ_inj`

---
 Iris/Iris/Algebra/StepIndex.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 2ca10cdbb..7d4f0d4ce 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -122,8 +122,6 @@ theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
   · exact inst.lt_trans h1 h2
   · subst h1; assumption
 
--- instance succ_inj : Function.Injective Eq Eq (fun x => succᵢ x)
-
 @[rocq_alias SIdx.le_succ_diag_r]
 theorem le_succ_diag_r : n ≤ succᵢ n := by
   apply lt_le_incl
@@ -179,6 +177,10 @@ theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := by
 theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := by
   rewrite [lt_succ_r, le_succ_l]; rfl
 
+@[rocq_alias SIdx.succ_inj]
+theorem succ_inj (h : succᵢ n = succᵢ m) : n = m := by
+  apply le_antisymm <;> apply succ_le_mono.mpr <;> rw [h]
+
 @[rocq_alias SIdx.nlt_succ_r]
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := by
   rw [lt_succ_r, lt_nge]

From b2c2db55bdbac6a53d0757d86e50ebe4b8410174 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 16:54:24 +0200
Subject: [PATCH 18/24] Code reorganisation

---
 Iris/Iris/Algebra/StepIndex.lean | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 7d4f0d4ce..624ebdd52 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -12,7 +12,7 @@ public import Iris.Std.Classes
 
 namespace Iris
 
-@[rocq_alias sidx]
+@[rocq_alias sidx, rocq_alias SIdxMixin]
 class SIdx (I : Type u) extends LT I, LE I, Zero I where
   succ : I → I
   lt_trans : ∀ {n m p : I}, n < m → m < p → n < p
@@ -30,22 +30,17 @@ scoped prefix:max "succᵢ" => SIdx.succ
 class SIdxFinite (I : Type u) [SIdx I] : Prop where
   finite_index : ∀ n : I, n = 0 ∨ ∃ m, n = succᵢ m
 
-#rocq_ignore SIdxMixin "Use the type class SIdx instead"
-
 namespace SIdx
 
 open Iris Std
 
 variable {I : Type u} [inst : SIdx I] {m n p : I}
 
-@[rocq_alias SIdx.nlt_0_r]
-theorem nlt_0_r (n : I) : ¬n < 0 := inst.not_lt_zero n
-
 @[rocq_alias SIdx.lt_succ_diag_r]
 theorem lt_succ_diag_r (n : I) : n < succᵢ n := inst.lt_succ_self n
 
-@[rocq_alias SIdx.le_succ_l_2]
-theorem le_succ_l_2 (h : n < m) : succᵢ n ≤ m := inst.succ_le_of_lt h
+@[rocq_alias SIdx.lt_succ_diag_r']
+theorem lt_succ_diag_r' (n : I) : n < succᵢ n := inst.lt_succ_diag_r n
 
 @[rocq_alias SIdx.inhabited]
 instance inhabited : Inhabited I where
@@ -62,7 +57,7 @@ theorem lt_asymm (h : n < m) : ¬m < n := by
   exact inst.lt_trans h h1
 
 @[rocq_alias SIdx.lt_strict]
-instance lt_struct : StrictOrder inst.lt where
+instance lt_strict : StrictOrder inst.lt where
   irrefl := by intro n; exact lt_irrefl n
   trans := inst.lt_trans
 
@@ -153,6 +148,9 @@ theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := by
     apply h2
     exact le_antisymm h1 h3
 
+@[rocq_alias SIdx.le_succ_l_2]
+theorem le_succ_l_2 (h : n < m) : succᵢ n ≤ m := inst.succ_le_of_lt h
+
 @[rocq_alias SIdx.le_succ_l]
 theorem le_succ_l : succᵢ n ≤ m ↔ n < m := by
   constructor <;> intro h
@@ -181,6 +179,9 @@ theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := by
 theorem succ_inj (h : succᵢ n = succᵢ m) : n = m := by
   apply le_antisymm <;> apply succ_le_mono.mpr <;> rw [h]
 
+@[rocq_alias SIdx.nlt_0_r]
+theorem nlt_0_r (n : I) : ¬n < 0 := inst.not_lt_zero n
+
 @[rocq_alias SIdx.nlt_succ_r]
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := by
   rw [lt_succ_r, lt_nge]

From 60232a82f0a33431df62ffe42f7078e3aa4c2d77 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 16:54:37 +0200
Subject: [PATCH 19/24] Remove `StepIndexFinite.lean`: to be ported later

---
 Iris/Iris/Algebra.lean                 |  1 -
 Iris/Iris/Algebra/StepIndexFinite.lean | 12 ------------
 2 files changed, 13 deletions(-)
 delete mode 100644 Iris/Iris/Algebra/StepIndexFinite.lean

diff --git a/Iris/Iris/Algebra.lean b/Iris/Iris/Algebra.lean
index 713772252..98a25050b 100644
--- a/Iris/Iris/Algebra.lean
+++ b/Iris/Iris/Algebra.lean
@@ -12,7 +12,6 @@ public import Iris.Algebra.LocalUpdates
 public import Iris.Algebra.IProp
 public import Iris.Algebra.OFE
 public import Iris.Algebra.StepIndex
-public import Iris.Algebra.StepIndexFinite
 public import Iris.Algebra.UFrac
 public import Iris.Algebra.Updates
 public import Iris.Algebra.UPred
diff --git a/Iris/Iris/Algebra/StepIndexFinite.lean b/Iris/Iris/Algebra/StepIndexFinite.lean
deleted file mode 100644
index b7e7377fb..000000000
--- a/Iris/Iris/Algebra/StepIndexFinite.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-/-
-Copyright (c) 2026 Alvin Tang. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler, Alvin Tang
--/
-module
-
-public meta import Iris.Std.RocqPorting
-
-@[expose] public section
-
-namespace Iris

From cba8474abf235ef0bf6d1b8d5ee7540865b1418e Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 17:14:25 +0200
Subject: [PATCH 20/24] Add `rocq_ignore` entries, add decidability instances

---
 Iris/Iris/Algebra/StepIndex.lean | 78 +++++++++++++++++++++++++-------
 1 file changed, 61 insertions(+), 17 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 624ebdd52..d4c648ee4 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -30,17 +30,26 @@ scoped prefix:max "succᵢ" => SIdx.succ
 class SIdxFinite (I : Type u) [SIdx I] : Prop where
   finite_index : ∀ n : I, n = 0 ∨ ∃ m, n = succᵢ m
 
+#rocq_ignore lt_trans "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore lt_wf "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore lt_lteq "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore lt_trichotomy "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore le_lteq "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore nlt_0_r "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore lt_succ_diag_r "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore le_succ_l_2 "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore weak_case "Lifting of mixin properties not required as they are part of the type class"
+
 namespace SIdx
 
 open Iris Std
 
 variable {I : Type u} [inst : SIdx I] {m n p : I}
 
-@[rocq_alias SIdx.lt_succ_diag_r]
-theorem lt_succ_diag_r (n : I) : n < succᵢ n := inst.lt_succ_self n
-
 @[rocq_alias SIdx.lt_succ_diag_r']
-theorem lt_succ_diag_r' (n : I) : n < succᵢ n := inst.lt_succ_diag_r n
+theorem lt_succ_diag_r' (h : n = succᵢ m) : m < n := by
+  subst h
+  exact inst.lt_succ_self m
 
 @[rocq_alias SIdx.inhabited]
 instance inhabited : Inhabited I where
@@ -120,7 +129,7 @@ theorem le_lt_trans (h1 : n ≤ m) (h2 : m < p) : n < p := by
 @[rocq_alias SIdx.le_succ_diag_r]
 theorem le_succ_diag_r : n ≤ succᵢ n := by
   apply lt_le_incl
-  apply lt_succ_diag_r
+  apply inst.lt_succ_self
 
 @[rocq_alias SIdx.le_ngt]
 theorem le_ngt : n ≤ m ↔ ¬ m < n := by
@@ -148,14 +157,11 @@ theorem le_neq : n < m ↔ n ≤ m ∧ n ≠ m := by
     apply h2
     exact le_antisymm h1 h3
 
-@[rocq_alias SIdx.le_succ_l_2]
-theorem le_succ_l_2 (h : n < m) : succᵢ n ≤ m := inst.succ_le_of_lt h
-
 @[rocq_alias SIdx.le_succ_l]
 theorem le_succ_l : succᵢ n ≤ m ↔ n < m := by
   constructor <;> intro h
   · exact lt_le_trans (lt_succ_self n) h
-  · exact le_succ_l_2 h
+  · exact succ_le_of_lt h
 
 @[rocq_alias SIdx.lt_succ_r]
 theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := by
@@ -164,8 +170,8 @@ theorem lt_succ_r : n < succᵢ m ↔ n ≤ m := by
     intro h1
     apply lt_irrefl n
     apply lt_le_trans h
-    exact le_succ_l_2 h1
-  · exact le_lt_trans h <| lt_succ_diag_r m
+    exact succ_le_of_lt h1
+  · exact le_lt_trans h <| inst.lt_succ_self m
 
 @[rocq_alias SIdx.succ_le_mono]
 theorem succ_le_mono : n ≤ m ↔ succᵢ n ≤ succᵢ m := by
@@ -179,15 +185,12 @@ theorem succ_lt_mono : n < m ↔ succᵢ n < succᵢ m := by
 theorem succ_inj (h : succᵢ n = succᵢ m) : n = m := by
   apply le_antisymm <;> apply succ_le_mono.mpr <;> rw [h]
 
-@[rocq_alias SIdx.nlt_0_r]
-theorem nlt_0_r (n : I) : ¬n < 0 := inst.not_lt_zero n
-
 @[rocq_alias SIdx.nlt_succ_r]
 theorem nlt_succ_r : ¬ m < succᵢ n ↔ n < m := by
   rw [lt_succ_r, lt_nge]
 
 @[rocq_alias SIdx.le_0_l]
-theorem le_0_l : 0 ≤ n := le_ngt.mpr <| nlt_0_r n
+theorem le_0_l : 0 ≤ n := le_ngt.mpr <| inst.not_lt_zero n
 
 @[rocq_alias SIdx.le_0_r]
 theorem le_0_r : n ≤ 0 ↔ n = 0 := by
@@ -205,7 +208,7 @@ theorem neq_0_lt_0 : n ≠ 0 ↔ 0 < n := by
     · assumption
     · exact absurd (le_0_r.mp h1) h
   · rintro h rfl
-    exact inst.nlt_0_r 0 h
+    exact inst.not_lt_zero 0 h
 
 @[rocq_alias neq_succ_0]
 theorem neq_succ_0 : succᵢ n ≠ 0 := neq_0_lt_0.mpr <| lt_succ_r.mpr le_0_l
@@ -213,8 +216,49 @@ theorem neq_succ_0 : succᵢ n ≠ 0 := neq_0_lt_0.mpr <| lt_succ_r.mpr le_0_l
 @[rocq_alias succ_neq]
 theorem succ_neq : n ≠ succᵢ n := by
   intro h
-  have hlt := inst.lt_succ_diag_r n
+  have hlt := inst.lt_succ_self n
   rw [← h] at hlt
   exact lt_irrefl n hlt
 
+@[rocq_alias SIdx.eq_dec]
+instance (priority := low) eqDec : DecidableEq I := fun n m =>
+  match inst.lt_trichotomyT n m with
+  | .inl h => by
+    apply isFalse
+    rintro rfl
+    exact lt_irrefl n h
+  | .inr (.inl h) => isTrue h
+  | .inr (.inr h) => by
+    apply isFalse
+    rintro rfl
+    exact lt_irrefl n h
+
+@[rocq_alias SIdx.lt_dec]
+instance (priority := low) (n m : I) : Decidable (n < m) :=
+  match inst.lt_trichotomyT n m with
+  | .inl h => isTrue h
+  | .inr (.inl h) => by
+    apply isFalse
+    rintro h'
+    subst h
+    exact lt_irrefl n h'
+  | .inr (.inr h) => by
+    apply isFalse
+    intro h'
+    exact lt_irrefl m <| inst.lt_trans h h'
+
+@[rocq_alias SIdx.le_dec]
+instance (priority := low) (n m : I) : Decidable (n ≤ m) :=
+  match inst.lt_trichotomyT n m with
+  | .inl h => by
+    apply isTrue
+    exact lt_le_incl h
+  | .inr (.inl h) => by
+    apply isTrue
+    exact le_lteq.mpr <| .inr h
+  | .inr (.inr h) => by
+    apply isFalse
+    intro h'
+    exact lt_irrefl m <| lt_le_trans h h'
+
 end SIdx

From b762bd10fe16ab2a950206828f843db407645030 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 17:40:55 +0200
Subject: [PATCH 21/24] Fix `rocq_ignore` entries, port `SIdx.limit`

---
 Iris/Iris/Algebra/StepIndex.lean | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index d4c648ee4..ba2013a18 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -27,18 +27,18 @@ class SIdx (I : Type u) extends LT I, LE I, Zero I where
 /-- The step-indexing successor operator. -/
 scoped prefix:max "succᵢ" => SIdx.succ
 
-class SIdxFinite (I : Type u) [SIdx I] : Prop where
+class SIdxFinite (I : Type u) [SIdx I] where
   finite_index : ∀ n : I, n = 0 ∨ ∃ m, n = succᵢ m
 
-#rocq_ignore lt_trans "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore lt_wf "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore lt_lteq "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore lt_trichotomy "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore le_lteq "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore nlt_0_r "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore lt_succ_diag_r "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore le_succ_l_2 "Lifting of mixin properties not required as they are part of the type class"
-#rocq_ignore weak_case "Lifting of mixin properties not required as they are part of the type class"
+#rocq_ignore SIdx.t_trans "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.lt_wf "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.lt_lteq "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.lt_trichotomy "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.le_lteq "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.nlt_0_r "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.lt_succ_diag_r "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.le_succ_l_2 "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.weak_case "Lifting of mixin properties not required as they are part of the type class SIdx"
 
 namespace SIdx
 
@@ -261,4 +261,9 @@ instance (priority := low) (n m : I) : Decidable (n ≤ m) :=
     intro h'
     exact lt_irrefl m <| lt_le_trans h h'
 
+@[rocq_alias SIdx.limit]
+structure Limit (n : I) [SIdx I] where
+  succ_lt : ∀ m, m < n → succᵢ m < n
+  ne_zero : n ≠ 0
+
 end SIdx

From fc7a175d8aa8c3d0102bb7542d84565532996a41 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 14 Jul 2026 17:51:48 +0200
Subject: [PATCH 22/24] Port `limit_0`, `limit_lt_0`, `limit_S`, `limit_finite`

---
 Iris/Iris/Algebra/StepIndex.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index ba2013a18..ea4ca3364 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -266,4 +266,29 @@ structure Limit (n : I) [SIdx I] where
   succ_lt : ∀ m, m < n → succᵢ m < n
   ne_zero : n ≠ 0
 
+@[simp, rocq_alias SIdx.limit_0]
+theorem limit_0 : ¬Limit (0 : I) := by
+  intro h
+  exact h.ne_zero rfl
+
+@[rocq_alias SIdx.limit_lt_0]
+theorem Limit.limit_lt_0 (h : Limit n) : 0 < n := neq_0_lt_0.mp h.ne_zero
+
+@[simp, rocq_alias SIdx.limit_S]
+theorem limit_S (n : I) : ¬Limit (succᵢ n) := by
+  intro h
+  apply lt_irrefl (succᵢ n)
+  apply h.succ_lt n
+  exact lt_succ_self n
+
+@[rocq_alias SIdx.limit_finite]
+theorem limit_finite [inst : SIdxFinite I] (n : I) : ¬Limit n := by
+  intro h
+  rcases SIdxFinite.finite_index n with (h0 | h0)
+  · exact h.ne_zero h0
+  · rcases h0 with ⟨m, hm⟩
+    apply limit_S m
+    subst hm
+    assumption
+
 end SIdx

From 829f437e8120b9e0301767b2da18825f9a3ecd70 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 15 Jul 2026 17:36:24 +0200
Subject: [PATCH 23/24] Port the `rec` and the remaining theorems

---
 Iris/Iris/Algebra/StepIndex.lean | 77 ++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index ea4ca3364..35d0c7a1e 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -291,4 +291,81 @@ theorem limit_finite [inst : SIdxFinite I] (n : I) : ¬Limit n := by
     subst hm
     assumption
 
+@[rocq_alias SIdx.case]
+def case (n : I) : (n = 0) ⊕' (Σ' m, n = succᵢ m) ⊕' Limit n :=
+  if h : n = 0 then .inl h
+  else
+    match inst.weak_case n with
+    | .inl ⟨m, hm⟩ => .inr <| .inl ⟨m, hm⟩
+    | .inr hlim => .inr <| .inr ⟨hlim, h⟩
+
+@[rocq_alias SIdx.rec]
+def rec' {P : I → Sort v}
+    (s : P 0)
+    (f : ∀ n, P n → P (succᵢ n))
+    (lim : ∀ n, Limit n → (∀ m, m < n → P m) → P n) :
+    ∀ n, P n :=
+  WellFounded.fix inst.lt_wf fun n IH =>
+    match SIdx.case n with
+    | .inl EQ => EQ ▸ s
+    | .inr <| .inl ⟨m, EQ⟩ => EQ ▸ f m (IH m (lt_succ_diag_r' EQ))
+    | .inr <| .inr Hlim => lim n Hlim IH
+
+@[rocq_alias SIdx.rec_unfold]
+theorem rec_unfold {P : I → Sort v} (s : P 0) (f : ∀ n, P n → P (succᵢ n))
+    (lim : ∀ n, Limit n → (∀ m, m < n → P m) → P n) (n : I) :
+    rec' s f lim n =
+      match SIdx.case n with
+      | .inl EQ => EQ ▸ s
+      | .inr (.inl ⟨m, EQ⟩) => EQ ▸ f m (rec' s f lim m)
+      | .inr (.inr Hlim) => lim n Hlim (fun m _ => rec' s f lim m) :=
+  inst.lt_wf.fix_eq _ n
+
+@[rocq_alias SIdx.rec_zero]
+theorem rec_zero {P : I → Sort v} (s : P 0) (f : ∀ n, P n → P (succᵢ n))
+    (lim : ∀ n, Limit n → (∀ m, m < n → P m) → P n) :
+    rec' s f lim 0 = s := by
+  rw [rec_unfold s f lim 0]
+  cases SIdx.case (0 : I) with
+  | inl EQ => rfl
+  | inr h =>
+    cases h with
+    | inl h =>
+      let ⟨m, EQ⟩ := h
+      exact absurd EQ.symm neq_succ_0
+    | inr Hlim => exact absurd Hlim limit_0
+
+@[rocq_alias SIdx.rec_succ]
+theorem rec_succ {P : I → Sort v} (s : P 0) (f : ∀ n, P n → P (succᵢ n))
+    (lim : ∀ n, Limit n → (∀ m, m < n → P m) → P n) (n : I) :
+    rec' s f lim (succᵢ n) = f n (rec' s f lim n) := by
+  rw [rec_unfold s f lim (succᵢ n)]
+  cases SIdx.case (succᵢ n) with
+  | inl EQ => exact absurd EQ neq_succ_0
+  | inr h =>
+    cases h with
+    | inl h =>
+      obtain ⟨m, EQ⟩ := h
+      obtain rfl := succ_inj EQ
+      rfl
+    | inr Hlim => exact absurd Hlim (limit_S n)
+
+@[rocq_alias SIdx.rec_lim]
+theorem rec_lim {P : I → Sort v} (s : P 0) (f : ∀ n, P n → P (succᵢ n))
+    (lim : ∀ n, Limit n → (∀ m, m < n → P m) → P n) (n : I) (Hn : Limit n) :
+    rec' s f lim n = lim n Hn (fun m _ => rec' s f lim m) := by
+  rw [rec_unfold s f lim n]
+  cases SIdx.case n with
+  | inl EQ => exact absurd EQ Hn.ne_zero
+  | inr h =>
+    cases h with
+    | inl h =>
+      obtain ⟨m, EQ⟩ := h
+      exact absurd (EQ ▸ Hn) (limit_S m)
+    | inr Hlim => rfl
+
+#rocq_ignore rec_lim_ext
+  "Proof irrelevance already handled automatically by Lean for the theorems \
+  rec_zero, rec_succ and rec_elim"
+
 end SIdx

From 9f32bc770fe5c95dfd7b2fb6f7d4c3e0dd865906 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Wed, 15 Jul 2026 17:37:34 +0200
Subject: [PATCH 24/24] Typo fix

---
 Iris/Iris/Algebra/StepIndex.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Iris/Iris/Algebra/StepIndex.lean b/Iris/Iris/Algebra/StepIndex.lean
index 35d0c7a1e..1fdd8feb0 100644
--- a/Iris/Iris/Algebra/StepIndex.lean
+++ b/Iris/Iris/Algebra/StepIndex.lean
@@ -30,7 +30,7 @@ scoped prefix:max "succᵢ" => SIdx.succ
 class SIdxFinite (I : Type u) [SIdx I] where
   finite_index : ∀ n : I, n = 0 ∨ ∃ m, n = succᵢ m
 
-#rocq_ignore SIdx.t_trans "Lifting of mixin properties not required as they are part of the type class SIdx"
+#rocq_ignore SIdx.lt_trans "Lifting of mixin properties not required as they are part of the type class SIdx"
 #rocq_ignore SIdx.lt_wf "Lifting of mixin properties not required as they are part of the type class SIdx"
 #rocq_ignore SIdx.lt_lteq "Lifting of mixin properties not required as they are part of the type class SIdx"
 #rocq_ignore SIdx.lt_trichotomy "Lifting of mixin properties not required as they are part of the type class SIdx"