diff --git a/Invariant.lean b/Invariant.lean
index edb75cf..13f2426 100644
--- a/Invariant.lean
+++ b/Invariant.lean
@@ -50,19 +50,20 @@ theorem list_insert_sorted (hs : List.Sorted (·<·) xs) : List.Sorted (·<·) (
     split
     · exact List.Sorted.of_cons hs
     · split
-      · rename_i hnlt
-        exact List.Sorted.cons hnlt hs
+      · exact List.Sorted.cons ‹_› hs
+      · have : a < x := by
+          rename_i hne hnlt
+          apply Nat.lt_of_le_of_ne
+          exact Nat.le_of_not_lt hnlt
+          exact fun a_1 => hne (Eq.symm a_1)
 
-      have : a < x := by
-        rename_i hne hnlt
-        apply Nat.lt_of_le_of_ne
-        exact Nat.le_of_not_lt hnlt
-        exact fun a_1 => hne (Eq.symm a_1)
+        simp only [List.sorted_cons]
 
-      have h : List.Sorted (·<·) as := List.Sorted.of_cons hs
-
-      have := ih h
-      sorry
+        constructor
+        · intro b hmem
+          cases list_insert_mem hmem
+          <;> simp_all only [imp_self, List.sorted_cons, and_true, not_lt]
+        · simp_all only [imp_self, List.sorted_cons, and_true, not_lt]
 
 def insert (x : ℕ) : NatSet → NatSet
 | ⟨[], _⟩ => singleton x