From 8fdf459876b999dbe184196f9abd330a3c24d560 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 4 Dec 2025 17:14:46 +0100
Subject: implement derivable equality

---
 Algebra/Terms.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'Algebra/Terms.lean')

diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean
index aa853a8..997dca4 100644
--- a/Algebra/Terms.lean
+++ b/Algebra/Terms.lean
@@ -87,6 +87,29 @@ def TermAtDepth.bound {n : ℕ} (a : 𝔸) (f : sig.bound) (args : sig.boundArgs
     TermAtDepth 𝔸 sig X (n + sig.boundDepth f) :=
   ⟨.bound a f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
 
+theorem TermAtDepth.induction
+  {motive : {n : ℕ} → TermAtDepth 𝔸 sig X n → Prop}
+  (var : ∀ (x : X), motive (.var x))
+  (pure : ∀ {n : ℕ} (f : sig.pure) (args : sig.pureArgs f → TermAtDepth 𝔸 sig X n),
+    (∀ x, motive (args x)) → motive (.pure f args))
+  (free : ∀ {n : ℕ} (a : 𝔸) (f : sig.free) (args : sig.freeArgs f → TermAtDepth 𝔸 sig X n),
+    (∀ x, motive (args x)) → motive (.free a f args))
+  (bound : ∀ {n : ℕ} (a : 𝔸) (f : sig.bound) (args : sig.boundArgs f → TermAtDepth 𝔸 sig X n),
+    (∀ x, motive (args x)) → motive (.bound a f args))
+  : ∀ {n : ℕ} (t : TermAtDepth 𝔸 sig X n), motive t := by
+  intro n ⟨t, ht⟩
+  induction' t generalizing n <;> cases ht <;> expose_names
+  · exact var x
+  · let args' : sig.pureArgs f → TermAtDepth 𝔸 sig X k := fun x => ⟨args x, h x⟩
+    have args_ih' : ∀ x, motive (args' x) := fun x => args_ih x (h x)
+    exact pure f args' args_ih'
+  · let args' : sig.freeArgs f → TermAtDepth 𝔸 sig X k := fun x => ⟨args x, h x⟩
+    have args_ih' : ∀ x, motive (args' x) := fun x => args_ih x (h x)
+    exact free a f args' args_ih'
+  · let args' : sig.boundArgs f → TermAtDepth 𝔸 sig X k := fun x => ⟨args x, h x⟩
+    have args_ih' : ∀ x, motive (args' x) := fun x => args_ih x (h x)
+    exact bound a f args' args_ih'
+
 end ConvenienceConstructors
 
 section Substitution
-- 
cgit v1.3.1