[DO NOT MERGE] Classifiers

.claude/settings.local.json

@@ -0,0 +1,7 @@
+{
+  "permissions": {
+    "allow": [
+      "Bash(lake build:*)"
+    ]
+  }
+}

Capless/Basic.lean

@@ -98,4 +98,7 @@ theorem FinFun.comp_succ {f : FinFun n n'}: Fin.succ ∘ f = (FinFun.ext f) ∘
 theorem FinFun.ext_zero {f : FinFun n n'} : f.ext 0 = 0 := by
   simp [FinFun.ext]
 
+theorem FinFun.ext_ext_one {f : FinFun n n'} : f.ext.ext 1 = 1 := by
+  rfl
+
 end Capless

Capless/CaptureBound.lean

@@ -0,0 +1,9 @@
+import Capless.CaptureSet
+import Capless.Type
+import Capless.Subcapturing
+
+namespace Capless
+
+inductive CaptureBound : Context n m k -> CaptureSet n k -> CBound n k -> Prop where
+  | subcapt: Subcapt Γ C1 C2 -> CaptureBound Γ C1 (CBound.upper C2)
+  | subkind : CaptureKind Γ C K -> CaptureBound Γ C (CBound.kind K)