# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483327802 0
# Node ID bf667ec8cba42e94726e4b50c2dafaba9ec4e63c
# Parent  d9b394c245c5ff53d501d5fb6b9fa0e74541a636
Set with constraint

diff -r d9b394c245c5 -r bf667ec8cba4 sandbox/SetWithConstraint.agda
--- a/sandbox/SetWithConstraint.agda	Mon Jan 02 03:17:18 2017 +0000
+++ b/sandbox/SetWithConstraint.agda	Mon Jan 02 03:30:02 2017 +0000
@@ -60,3 +60,16 @@
   ≡⟨ refl ⟩
   suc (suc (length s))
   ∎
+  
+insert-length-exists : (k : String) (n : ℕ )(s : MySet ℕ) {hasKey : elem k s ≡ true} {nonEmpty : s ≢ empty}
+                       -> length (insert (k , n) s) ≡ (length s)
+insert-length-exists _ _ empty  {nonEmpty = n}   = ⊥-elim (n refl)
+insert-length-exists k n (cons x s) {hasKey = h} = begin
+  length (insert (k , n) (cons x s))
+  ≡⟨ refl ⟩
+  length (insert' (elem k (cons x s)) (k , n) (cons x s))
+  ≡⟨ cong (\e -> length (insert' e (k , n) (cons x s))) h ⟩
+  length (insert' true (k , n) (cons x s))
+  ≡⟨ refl ⟩
+  length (cons x s)
+  ∎