From 6cd3c3cee7c20b3ba146d69051a35205e34f276c Mon Sep 17 00:00:00 2001
From: userName <userEmail>
Date: Mon, 20 Oct 2025 11:45:52 +0800
Subject: [PATCH] add explicit type parameter to set union theoremgit commit

---
 tbps-fe/lib/api.ts | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tbps-fe/lib/api.ts b/tbps-fe/lib/api.ts
index a487acd..29c2a61 100644
--- a/tbps-fe/lib/api.ts
+++ b/tbps-fe/lib/api.ts
@@ -128,11 +128,11 @@ export const EXAMPLE_EXPRESSIONS = [
   {
     name: "List Length Append",
     expression:
-      "∀ (l₁ l₂ : List α), List.length (l₁ ++ l₂) = List.length l₁ + List.length l₂",
+      "∀ (α : Type) (l₁ l₂ : List α), List.length (l₁ ++ l₂) = List.length l₁ + List.length l₂",
   },
   {
     name: "Set Union Commutativity",
-    expression: "∀ (A B : Set α), A ∪ B = B ∪ A",
+      expression: "∀ (α : Type) (A B : Set α), A ∪ B = B ∪ A",
   },
   {
     name: "Function Composition Associativity",
@@ -148,10 +148,10 @@ export const EXAMPLE_EXPRESSIONS = [
   },
   {
     name: "List Reverse Involutive",
-    expression: "∀ (l : List α), List.reverse (List.reverse l) = l",
+      expression: "∀ (α : Type) (l : List α), List.reverse (List.reverse l) = l",
   },
   {
     name: "Set Intersection Commutativity",
-    expression: "∀ (A B : Set α), A ∩ B = B ∩ A",
+      expression: "∀ (α : Type) (A B : Set α), A ∩ B = B ∩ A",
   },
 ];