From 4d8482addac93c3c5fceb991659b9895c1b754e7 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Tue, 4 Mar 2025 15:22:55 +0100
Subject: [PATCH 1/6] Added propExt.lp and funExt.lp, added nths and some
 theorems to list.lp

---
 Bool.lp    |  10 ++
 List.lp    |  76 +++++++++
 funExt.lp  |   4 +
 propExt.lp | 460 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 550 insertions(+)
 create mode 100644 funExt.lp
 create mode 100644 propExt.lp

diff --git a/Bool.lp b/Bool.lp
index 496fca0..76cbf1f 100644
--- a/Bool.lp
+++ b/Bool.lp
@@ -34,6 +34,16 @@ with istrue false ↪ ⊥;
 
 coerce_rule coerce 𝔹 Prop $x ↪ istrue $x;
 
+symbol istrue=true [x] : π (istrue x) → π (x = true)≔
+begin
+  assume x h;
+  refine ∨ₑ (case_𝔹 x) _ _
+      { assume h1; refine h1 }
+      { assume h1;
+      have H1: π (istrue false) { rewrite eq_sym h1; refine h };
+      refine ⊥ₑ H1 };
+end;
+
 // non confusion of constructors
 
 opaque symbol false≠true : π (false ≠ true) ≔
diff --git a/List.lp b/List.lp
index b49a934..6890f98 100644
--- a/List.lp
+++ b/List.lp
@@ -38,6 +38,9 @@ seqn n x_0 ... x_n-1 == the sequence of the x_i; can be partially applied.
  ** Random access:
         nth x0 s i == the item i of s (numbered from 0), or x0 if s does
                       not have at least i+1 items (i.e., size x <= i)
+      nths x0 s ks == the sequence that is formed when taking for each 
+                      index i in n the i-th item of ks (numbered from 0), 
+                      or x0 if s has fewer than i+1 items (i.e., size s <= i). 
               s`_i == standard notation for nth x0 s i for a default x0,
                       e.g., 0 for rings.
   set_nth x0 s i y == s where item i has been changed to y; if s does not
@@ -1083,6 +1086,21 @@ begin
   assume a beq x l hrefl; simplify; rewrite hrefl; apply ⊤ᵢ;
 end;
 
+opaque symbol mem_tail [a] (beq: τ a → τ a → 𝔹) (n m: τ a) (l: 𝕃 a) : 
+  π (∈ beq n l) → π (∈ beq n (m ⸬ l)) ≔
+begin
+  assume a beq n m; induction
+    {assume h1; refine ⊥ₑ h1}
+    {assume n0 l h1 h2;
+    have H0: π (beq n n0) →  π (beq n m or (beq n n0 or ∈ beq n l))
+      {assume h3;
+      refine orᵢ₂ (beq n m) [beq n n0 or ∈ beq n l] (orᵢ₁ [beq n n0] (∈ beq n l) h3)};
+    have H1: π (∈ beq n l) →  π (beq n m or (beq n n0 or ∈ beq n l))
+      {assume h3;
+      refine orᵢ₂ (beq n m) [beq n n0 or ∈ beq n l] (orᵢ₂ (beq n n0) [∈ beq n l] h3)};
+    refine orₑ [beq n n0] [∈ beq n l] (beq n m or (beq n n0 or ∈ beq n l)) h2 H0 H1}
+end;
+
 opaque symbol mem_take [a] beq n l (x:τ a) :
   π (∈ beq x (take n l)) → π (∈ beq x l) ≔
 begin
@@ -1591,6 +1609,64 @@ begin
   }
 end;
 
+// nths
+
+symbol nths [a : Set] : τ a → 𝕃 a → 𝕃 nat → 𝕃 a;
+
+rule nths $b $l $n ↪ map (nth $b $l) $n;
+
+opaque symbol mapS_iota (m n : τ nat) : 
+  π (map (+1) (iota n m) = iota (n +1) m)≔
+begin
+  induction
+    { induction
+      { refine eq_refl □ }
+      { assume n h; refine h } }
+    { induction
+      { assume h n; refine eq_refl (n +1 ⸬ □) }
+      { simplify; assume n0 h0 h1 m; rewrite h1 (m +1);
+      refine eq_refl (m +1 ⸬ m +1 +1 ⸬ iota (m +1 +1 +1) n0) } }
+end;
+
+opaque symbol indexes_cons [a : Set] (x : τ a) (l : 𝕃 a) : 
+  π (indexes (x ⸬ l) = 0 ⸬ (map (+1) (indexes l)))≔
+    begin
+      assume a x;
+      induction
+        { refine eq_refl (0 ⸬ □) }
+        { simplify;
+        assume y l h;
+        rewrite mapS_iota;
+        refine eq_refl (0 ⸬ 1 ⸬ iota 2 (size l)) }
+end;
+
+opaque symbol nths_shift_cons [a : Set] (x b : τ a) (l : 𝕃 a) (n : 𝕃 nat) : 
+  π ((nths b (x ⸬ l) (map (+1) n)) = (nths b l n))≔
+begin
+  assume a x b l; induction
+    { refine eq_refl □ }
+    { assume n ll h1;
+    have H1: π (nths b (x ⸬ l) (map (+1) (n ⸬ ll)) =
+      nth b (x ⸬ l) (n +1) ⸬ nths b (x ⸬ l) (map (+1) ll))
+      { refine eq_refl (nth b l n ⸬ map (nth b (x ⸬ l)) (map (+1) ll)) };
+    rewrite H1; rewrite h1;
+    refine eq_refl (nths b l (n ⸬ ll)) }
+end;
+
+opaque symbol nths_indexes_id [a : Set] (b : τ a) (l : 𝕃 a) : 
+  π (nths b l (indexes l) = l)≔
+begin
+  assume a b; induction
+  { refine eq_refl □ }
+  { assume x l h1;
+    rewrite indexes_cons x l;
+    have H1: π (nths b (x ⸬ l) (0 ⸬ map (+1) (indexes l)) =
+      x ⸬ nths b (x ⸬ l) (map (+1) (indexes l)))
+    { refine eq_refl (x ⸬ map (nth b (x ⸬ l)) (map (+1) (indexes l))) };
+    rewrite H1; rewrite nths_shift_cons x b l (indexes l); rewrite h1;
+    refine eq_refl (x ⸬ l) }
+end;
+
 // sumn
 
 symbol sumn : 𝕃 nat → ℕ;
diff --git a/funExt.lp b/funExt.lp
new file mode 100644
index 0000000..95605f7
--- /dev/null
+++ b/funExt.lp
@@ -0,0 +1,4 @@
+require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.FOL Stdlib.HOL;
+
+symbol funExt [T S] (f g : τ (T ⤳ S)) : π(`∀ x, f x = g x) → π(f = g);
+
diff --git a/propExt.lp b/propExt.lp
new file mode 100644
index 0000000..831e958
--- /dev/null
+++ b/propExt.lp
@@ -0,0 +1,460 @@
+/***************************************************************************
+This file provides an axiom and various theorems for propositional equality.        
+The theorems are grouped into sections by theme:  
+- Various Simplifications
+- Symmetry and polarity     
+- Equalities of propositions and equalities involving ⊤ and ⊥                                
+****************************************************************************/
+
+require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.Impred Stdlib.Classic;
+
+symbol propExt x y : (π x → π y) → (π y → π x) → π (x = y);
+
+
+/******************************************************************************
+ *  Simplifications          
+ ******************************************************************************/
+
+// Idempotence and Contradiction for ∧ and ∨
+
+opaque symbol ∨_idem x :
+  π (x = (x ∨ x)) ≔
+begin
+  assume x;
+  refine propExt x (x ∨ x) _ _
+    {assume h2; refine ∨ᵢ₁ h2}
+    {assume h1;
+     refine ∨ₑ h1 _ _
+       {assume h2; refine h2}
+       {assume h2; refine h2}}
+end;
+
+opaque symbol ∧_idem x :
+  π (x = (x ∧ x)) ≔
+begin
+  assume x;
+  refine propExt x (x ∧ x) _ _
+    {assume h1; refine ∧ᵢ h1 h1}
+    {assume h1; refine ∧ₑ₁ h1}
+end;
+
+opaque symbol ∧_contra x :
+  π (⊥ = (¬ x ∧ x)) ≔
+begin
+  assume x;
+  refine propExt ⊥ (¬ x ∧ x) _ _
+    {assume h1; refine ⊥ₑ h1}
+    {assume h1;
+     refine (∧ₑ₁ h1) (∧ₑ₂ h1)}
+end;
+
+
+// Disjunction/Conjunction with ⊤ / ⊥      
+
+opaque symbol ∨⊤ x :
+  π (⊤ = (x ∨ ⊤)) ≔
+begin
+  assume x;
+  refine propExt ⊤ (x ∨ ⊤) _ _
+    {assume h2; refine ∨ᵢ₂ h2}
+    {assume h1; refine ⊤ᵢ}
+end;
+
+opaque symbol ∧⊤ x :
+  π (x = (x ∧ ⊤)) ≔
+begin
+  assume x;
+  refine propExt x (x ∧ ⊤) _ _
+    {assume h1; refine ∧ᵢ h1 ⊤ᵢ}
+    {assume h1; refine ∧ₑ₁ h1}
+end;
+
+opaque symbol ∨⊥ x :
+  π (x = (x ∨ ⊥)) ≔
+begin
+  assume x;
+  refine propExt x (x ∨ ⊥) _ _
+    {assume h1; refine ∨ᵢ₁ h1}
+    {assume h1;
+     refine ∨ₑ h1 _ _
+       {assume h2; refine h2}
+       {assume h2; refine ⊥ₑ h2}}
+end;
+
+opaque symbol ∧⊥ x :
+  π (⊥ = (x ∧ ⊥)) ≔
+begin
+  assume x;
+  refine propExt ⊥ (x ∧ ⊥) _ _
+    {assume h1;
+     type ⊥ₑ h1;
+     refine ∧ᵢ (⊥ₑ h1) h1}
+    {assume h1; refine ∧ₑ₂ h1}
+end;
+
+
+// Negation of ⊤ and ⊥  
+
+opaque symbol ¬⊥ :
+  π (⊤ = ¬ ⊥) ≔
+begin
+  refine propExt ⊤ (¬ ⊥) _ _
+    {assume h1 h2; refine h2}
+    {assume h1; refine ⊤ᵢ}
+end;
+
+opaque symbol ¬⊤ :
+  π (⊥ = ¬ ⊤) ≔
+begin
+  refine propExt ⊥ (¬ ⊤) _ _
+    {assume h1; refine ⊥ₑ h1}
+    {assume h1; refine h1 ⊤ᵢ}
+end;
+
+
+//Equalities on Elements   
+
+opaque symbol eq_refl_top (T : Set) (x : τ T) :
+  π (⊤ = (x = x)) ≔
+begin
+  assume T x;
+  refine propExt ⊤ (x = x) _ _
+    {assume h1; refine eq_refl x}
+    {assume h1; refine ⊤ᵢ}
+end;
+
+opaque symbol eq_refl_bot (T : Set) (x : τ T) :
+  π (⊥ = ¬ (x = x)) ≔
+begin
+  assume T x;
+  refine propExt ⊥ (¬ (x = x)) _ _
+    {assume h1; refine ⊥ₑ h1}
+    {assume h1;
+     have H1: π(x = x) → π ⊥
+       {assume h2; refine h1 h2};
+     refine H1 (eq_refl [T] x)}
+end;
+
+opaque symbol eq⊤ x :
+  π (x = (x = ⊤)) ≔
+begin
+  assume x;
+  refine propExt x (x = ⊤) _ _
+    {assume h1;
+     refine propExt x ⊤ _ _
+        {assume h2; refine ⊤ᵢ}
+        {assume h2; refine h1}}
+    {assume h1;
+     refine (ind_eq h1 (λ z, z)) ⊤ᵢ}
+end;
+
+opaque symbol ¬eq⊤ x :
+  π (¬ x = ¬(x = ⊤)) ≔
+begin
+  assume x;
+  refine propExt (¬ x) (¬(x = ⊤)) _ _
+    {assume h1 h2;
+     have H1_1: π x
+       {refine ind_eq h2 (λ z, z) ⊤ᵢ};
+     refine h1 H1_1}
+    {assume h1 h2;
+     refine h1 (propExt x ⊤ _ _)
+        {assume h3; refine ⊤ᵢ}
+        {assume h3; refine h2}}
+end;
+
+
+// Simplifications reflecting Classical Principles
+
+opaque symbol em_eq x :
+  π (⊤ = (¬ x ∨ x)) ≔
+begin
+  assume x;
+  refine propExt ⊤ (¬ x ∨ x) _ _
+    {assume h1;
+     have em_sym: π(¬ x ∨ x)
+       {refine ∨ₑ (em x) _ _
+         {assume h3; refine ∨ᵢ₂ h3}
+         {assume h3; refine ∨ᵢ₁ h3}};
+     refine em_sym}
+    {assume h1; refine ⊤ᵢ}
+end;
+
+opaque symbol ¬¬ₑ_eq x :
+  π (x = ¬ ¬ x) ≔
+begin
+  assume x;
+  refine propExt x (¬ ¬ x) _ _
+    {assume h1 h2; refine h2 h1}
+    {assume h1; refine ¬¬ₑ x h1}
+end;
+
+
+/******************************************************************************
+ *  Symmetry and polarity                                                     
+ ******************************************************************************/
+
+ opaque symbol eq_sym_eq [T] (x y : τ T) :
+ π((x = y) = (y = x)) ≔
+begin
+ assume T x y;
+ have H1: π(x = y) → π(y = x)
+   {assume h; symmetry; refine h};
+ have H2: π(y = x) → π(x = y)
+   {assume h; symmetry; refine h};
+ refine propExt (x = y) (y = x) H1 H2
+end;
+
+symbol polarity_switch a b :
+ π ((a = b) = (¬ a = ¬ b)) ≔
+begin
+ assume a b;
+ refine propExt (a = b) (¬ a = ¬ b) _ _
+   {assume h1;
+    have H1: π(b = a)
+      {symmetry; refine h1};
+    refine propExt (¬ a) (¬ b) _ _
+      {assume h2; refine ind_eq H1 (λ x, ¬ x) h2}
+      {assume h2; refine ind_eq h1 (λ x, ¬ x) h2}}
+   {assume h1;
+    have H1: π(¬ b = ¬ a)
+      {symmetry; refine h1};
+    refine propExt a b _ _
+      {assume h2;
+       have H2: π(¬ ¬ a)
+         {assume h3; refine h3 h2};
+       refine (¬¬ₑ b) (ind_eq H1 (λ x, ¬ x) H2)}
+      {assume h2;
+       have H2: π(¬ (¬ b))
+         {assume h3; refine h3 h2};
+       refine (¬¬ₑ a) (ind_eq h1 (λ x, ¬ x) H2)}}
+end;
+
+
+/******************************************************************************
+*  Equalities of propositions and equalities involving ⊤ and ⊥                              
+******************************************************************************/
+
+// Propositions on the LHS
+
+opaque symbol posProp_posEqT x :
+  π (x = (x = ⊤)) ≔
+begin
+  assume x;
+  refine propExt x (x = ⊤) _ _
+    {assume h1;
+     refine propExt x ⊤ _ _
+       {assume h2; refine ⊤ᵢ}
+       {assume h2; refine h1}}
+    {assume h2;
+     refine ind_eq h2 (λ z, z) ⊤ᵢ}
+end;
+
+opaque symbol posProp_negEqT x :
+  π (x = ¬(¬ x = ⊤)) ≔
+begin
+  assume x;
+  refine propExt x (¬(¬ x = ⊤)) _ _
+    {assume h1 h2;
+     refine ((ind_eq h2 (λ z, z)) ⊤ᵢ) h1}
+    {assume h1;
+     refine ∨ₑ [x] [¬ x] [x] (em x) _ _
+       {assume h2; refine h2}
+       {assume h2;
+        have H1: π(¬ x = ⊤)
+          {refine propExt (¬ x) ⊤ _ _
+            {assume h3; refine ⊤ᵢ}
+            {assume h3; refine h2}};
+        refine ⊥ₑ (h1 H1)}}
+end;
+
+opaque symbol negProp_posEqT x :
+  π (¬ x = (¬ x = ⊤)) ≔
+begin
+  assume x;
+  refine propExt (¬ x) (¬ x = ⊤) _ _
+    {assume h1;
+     refine propExt (¬ x) ⊤ _ _
+        {assume h2; refine ⊤ᵢ}
+        {assume h2; refine h1}}
+    {assume h1;
+     have H1: π(¬ x = ⊤) → π(¬ x)
+       {assume h2;
+        refine (ind_eq h2 (λ z, z)) ⊤ᵢ};
+     refine H1 h1}
+end;
+
+opaque symbol negProp_negEqT x :
+  π (¬ x = ¬(x = ⊤)) ≔
+begin
+  assume x;
+  refine propExt (¬ x) (¬ (x = ⊤)) _ _
+    {assume h1 h2;
+     refine h1 (ind_eq h2 (λ z, z) ⊤ᵢ)}
+    {assume h1 h2;
+     have H1: π(x = ⊤)
+       {refine propExt x ⊤ _ _
+        {assume h3; refine ⊤ᵢ}
+        {assume h3; refine h2}};
+     refine h1 H1}
+end;
+
+opaque symbol negProp_posEqB x :
+  π (¬ x = (x = ⊥)) ≔
+begin
+  assume x;
+  type propExt (¬ x) (x = ⊥) _ _;
+  refine propExt (¬ x) (x = ⊥) _ _
+    {assume h1;
+     refine propExt x ⊥ _ _
+       {assume h2; refine h1 h2}
+       {assume h2; refine ⊥ₑ h2}}
+    {assume h1;
+     refine ind_eq h1 (λ y, ¬ y) (λ h: π ⊥, h)}
+end;
+
+opaque symbol negProp_negEqB x :
+  π (¬ x = ¬(¬ x = ⊥)) ≔
+begin
+  assume x;
+  refine propExt (¬ x) (¬(¬ x = ⊥)) _ _
+    {assume h1 h2;
+     have H1: π(⊥ = ¬ x)
+       {symmetry; refine h2};
+     refine ind_eq H1 (λ y, y) h1}
+    {assume h1 h2;
+     refine h1 _;
+     refine propExt (¬ x) ⊥ _ _
+       {assume h3; refine h3 h2}
+       {assume h3; refine ⊥ₑ h3}}
+end;
+
+opaque symbol posProp_negEqB x :
+  π (x = ¬(x = ⊥)) ≔
+begin
+  assume x;
+  refine propExt x (¬ (x = ⊥)) _ _
+    {assume h1 h2;
+     refine ind_eq h2 (λ z, z ⇒ ⊥) (λ y: π ⊥, y) h1}
+    {assume h1;
+     refine ¬¬ₑ x _;
+     assume h2;
+     have H1: π(x = ⊥)
+       {refine propExt x ⊥ _ _
+         {assume h3; refine h2 h3}
+         {assume h3; refine ⊥ₑ h3}};
+     refine h1 H1}
+end;
+
+opaque symbol posProp_posEqB x :
+  π (x = (¬ x = ⊥)) ≔
+begin
+  assume x;
+  refine propExt x (¬ x = ⊥) _ _
+    {assume h1;
+     refine propExt (¬ x) ⊥ _ _
+       {assume h2; refine h2 h1}
+       {assume h2; refine ⊥ₑ h2}}
+    {assume h1;
+     refine ¬¬ₑ x (ind_eq h1 (λ y, ¬ y) (λ h: π ⊥, h))}
+end;
+
+
+// Equalities on the LHS
+
+opaque symbol negEqB_posProp x :
+  π (¬(¬ x = ⊤) = x) ≔
+begin
+  assume x;
+  symmetry;
+  refine propExt x (¬ (¬ x = ⊤)) _ _
+    {assume h1 h2;
+     refine ((ind_eq h2 (λ z, z)) ⊤ᵢ) h1}
+    {assume h1;
+     refine ∨ₑ (em x) _ _
+        {assume h2; refine h2}
+        {assume h2;
+         have H1: π(¬ x = ⊤)
+          {refine propExt (¬ x) ⊤ _ _
+            {assume h3; refine ⊤ᵢ}
+            {assume h3; refine h2}};
+         refine ⊥ₑ (h1 H1)}}
+end;
+
+opaque symbol negEqT_negProp x :
+  π (¬(x = ⊤) = ¬ x) ≔
+begin
+  assume x;
+  symmetry;
+  refine propExt (¬ x) (¬ (x = ⊤)) _ _
+    {assume h1 h2;
+     refine h1 (ind_eq h2 (λ z, z) ⊤ᵢ)}
+    {assume h1 h2;
+     have H1: π(x = ⊤)
+        {refine propExt x ⊤ _ _
+            {assume h3; refine ⊤ᵢ}
+            {assume h3; refine h2}};
+    refine h1 H1}
+end;
+
+opaque symbol posEqT_posProp x :
+  π ((x = ⊤) = x) ≔
+begin
+  assume x;
+  symmetry;
+  refine propExt x (x = ⊤) _ _
+    {assume h1;
+     refine propExt x ⊤ _ _
+        {assume h2; refine ⊤ᵢ}
+        {assume h2; refine h1}}
+    {assume h2;
+     refine ind_eq h2 (λ z, z) ⊤ᵢ}
+end;
+
+opaque symbol posEqT_negProp x :
+  π ((¬ x = ⊤) = ¬ x) ≔
+begin
+  assume x;
+  symmetry;
+  refine propExt (¬ x) (¬ x = ⊤) _ _
+    {assume h1;
+     refine propExt (¬ x) ⊤ _ _
+        {assume h2; refine ⊤ᵢ}
+        {assume h2; refine h1}}
+    {assume h1;
+     have H1: π(¬ x = ⊤) → π(¬ x)
+       {assume h2;
+        refine (ind_eq h2 (λ z, z)) ⊤ᵢ};
+     refine H1 h1}
+end;
+
+opaque symbol posEqT_l_posProp x :
+  π ((⊤ = x) = x) ≔
+begin
+  assume x;
+  refine propExt (⊤ = x) x _ _
+    {assume h1;
+     have H1: π x → π x
+       {assume h2; refine h2};
+     refine (ind_eq h1 (λ z, z ⇒ x) H1) ⊤ᵢ}
+    {assume h1;
+     refine propExt ⊤ x _ _
+        {assume h2; refine h1}
+        {assume h2; refine ⊤ᵢ}}
+end;
+
+opaque symbol posEqB_l_negProp x :
+  π ((⊥ = x) = ¬ x) ≔
+begin
+  assume x;
+  refine propExt (⊥ = x) (¬ x) _ _
+    {assume h1;
+     have H1: π x → π x
+       {assume h2; refine h2};
+     refine ind_eq h1 (λ z, x ⇒ z) H1}
+    {assume h1;
+     refine propExt ⊥ x _ _
+       {assume h2; refine ⊥ₑ h2}
+       {assume h2; refine h1 h2}}
+end;
+

From 92031f5d83d999476f41d35ef32eb389079297d5 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Tue, 4 Mar 2025 15:36:03 +0100
Subject: [PATCH 2/6] corrected name

---
 propExt.lp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/propExt.lp b/propExt.lp
index 831e958..74e7a88 100644
--- a/propExt.lp
+++ b/propExt.lp
@@ -362,7 +362,7 @@ end;
 
 // Equalities on the LHS
 
-opaque symbol negEqB_posProp x :
+opaque symbol negEqT_posProp x :
   π (¬(¬ x = ⊤) = x) ≔
 begin
   assume x;

From 28f1617b4b2a36b7db0e2d2b207344b0b2ec7e10 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <114103254+melanie-taprogge@users.noreply.github.com>
Date: Tue, 4 Mar 2025 15:37:30 +0100
Subject: [PATCH 3/6] Rename funExt.lp to FunExt.lp

---
 funExt.lp => FunExt.lp | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename funExt.lp => FunExt.lp (100%)

diff --git a/funExt.lp b/FunExt.lp
similarity index 100%
rename from funExt.lp
rename to FunExt.lp

From dec6851185f7b1c3ff587ff3538a6c96a8cc5dec Mon Sep 17 00:00:00 2001
From: melanie-taprogge <114103254+melanie-taprogge@users.noreply.github.com>
Date: Tue, 4 Mar 2025 15:38:05 +0100
Subject: [PATCH 4/6] Rename propExt.lp to PropExt.lp

---
 propExt.lp => PropExt.lp | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename propExt.lp => PropExt.lp (100%)

diff --git a/propExt.lp b/PropExt.lp
similarity index 100%
rename from propExt.lp
rename to PropExt.lp

From ab117433ebd7d6c46b6ad930cdbe4f639878b5da Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Wed, 5 Mar 2025 16:25:05 +0100
Subject: [PATCH 5/6] modify identifiers

---
 FunExt.lp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FunExt.lp b/FunExt.lp
index 95605f7..94204e8 100644
--- a/FunExt.lp
+++ b/FunExt.lp
@@ -1,4 +1,4 @@
 require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.FOL Stdlib.HOL;
 
-symbol funExt [T S] (f g : τ (T ⤳ S)) : π(`∀ x, f x = g x) → π(f = g);
+symbol funExt [a b] (f g : τ (a ⤳ b)) : π(`∀ x, f x = g x) → π(f = g);
 

From fb25801cfb704574b2bd761680da2de99778be8a Mon Sep 17 00:00:00 2001
From: melanie-taprogge <114103254+melanie-taprogge@users.noreply.github.com>
Date: Wed, 5 Mar 2025 19:35:47 +0100
Subject: [PATCH 6/6] Update CHANGES.md

---
 CHANGES.md | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 414ae8a..80e89fb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,6 +3,15 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+
+## Unreleased
+
+### Added
+
+- FunExt: Axiom for functional extensionality
+- PropExt: Axiom for propositional extensionality and related theorems
+- List: add nths
+
 ## 1.2.0 (2025-02-04)
 
 ### Added