just added some stuff

source/casestudies/2024-casestudy-lists/lists_case.mmt

@@ -57,8 +57,12 @@ theory ArrayLists =
 
     // equational theory???❙
     grow_update_eq : {m,l:array m, a,b,c} (grow l by a) update b as c ≐ grow (l update b as c) by a ❙
-    array_same : {a,x :a, l : array a, b,y:b, m : array b} x ≐ y ⟶ l ≐ m ❙
-    array_same_grow : {a, l: array a, m: array b,k :nat} l ≐ m ⟶ grow l by k ≐ grow m by k ❙
+    grow_make_eq
+    get_set_eq:
+
+
+    array_same : {a,l : array a, m : array a} length l = length m ⟶ ({n} n<length l ⟶ l get n = m get n) ⟶ l ≐ m  ❙
+    
     
     length : {a} array a ⟶ nat❘# | 2 |❙
     length_make : {a,n,x:a} |make n x| ≐ n❙
@@ -74,7 +78,7 @@ theory ArrayLists =
     get_set_eq: {a,x:a,l,n} (l update n as x) get n ≐ some x❙
     get_set_neq: {a,x:a,l,m,n} m ≠ n ⟶ (l update n as x) get m ≐ l get m ❙
     // some thing new from here❙
-    get_set_noteq : {a, x: a, l: array a, m, n} (l update m as x) get n ≠ x ⟶ m ≠ n ❙
+    get_noteq : {a, x: a, l: array a, m, n} ((l update m as x) get n) ≠ some x ⟶ m ≠ n ❙
 ❚
 
 theory SparseLists =