From d0ba090e345bffb28fb2cec56149e95fea01e10e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Luis=20Alberto=20D=C3=ADaz=20D=C3=ADaz?=
 <73986926+Luis-omega@users.noreply.github.com>
Date: Tue, 16 Apr 2024 14:08:23 -0600
Subject: [PATCH] added more clues to reduce admitted commands

---
 Grandpa/src/Dictionary.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Grandpa/src/Dictionary.v b/Grandpa/src/Dictionary.v
index 5f5a23b..ecbbba1 100644
--- a/Grandpa/src/Dictionary.v
+++ b/Grandpa/src/Dictionary.v
@@ -241,6 +241,26 @@ Proof.
 Qed.
 
 
+Lemma wellformed_means_unique_elements d (wf:WellFormedDict d) 
+  : forall k, 
+    count eqb_k k (map fst (to_list d)) <= 1.
+Proof.
+  destruct d as [l].
+  intro k.
+  induction l as [|[k2 v2] l Hind].
+  - simpl.
+    unfold count.
+    auto.
+  - simpl.
+    rewrite count_cons.
+    (*
+       proof 
+       WellFormedDict (DictionaryC l) -> DictionaryC l = from_list (rev l)
+       and use it with ++ in 
+       l = l1 ++ (k,v) :: l2 
+    *)
+    Admitted.
+
 Fixpoint eqb_aux (l: list (K * V)) (d:Dictionary K V) : bool
   :=
   match l with