Adding count lemma and further shorten.

theories/datatypes/List.ec

@@ -1659,6 +1659,10 @@ lemma count_uniq_mem s (x : 'a):
   uniq s => count (pred1 x) s = b2i (mem s x).
 proof. elim: s; smt(). qed.
 
+lemma count_mem_uniq (s : 'a list) :
+  (forall x, count (pred1 x) s = b2i (mem s x)) => uniq s.
+proof. elim s => //; smt(mem_count). qed. 
+
 lemma uniq_leq_size (s1 s2 : 'a list):
   uniq s1 => (mem s1 <= mem s2) => size s1 <= size s2.
 proof.                          (* FIXME: test case: for views *)
@@ -1685,19 +1689,14 @@ proof. by move=> /(uniq_le_perm_eq s1 s2) + eqmem eqsz; rewrite eqmem eqsz. qed.
 
 lemma perm_eq_uniq_impl (s1 s2 : 'a list) :
   perm_eq s1 s2 => uniq s1 => uniq s2.
-proof.  
-  elim: s2 s1 => // x l ih s ^ /perm_eqP_pred1 + + ^ /count_uniq_mem.
-  move=> /(_ x) + + /(_ x) => -> pmeq ^ cqeq + uqs.
-  have ^ xins -> @/b2i /= eqb2: x \in s by smt(count_ge0).
-  split; 1: by rewrite mem_count; 1: smt(count_ge0).
-  move/perm_eq_sym /(perm_eq_trans _ _ (x :: rem x s)): pmeq. 
-  rewrite perm_to_rem //= perm_cons => pmeq.
-  by rewrite (ih (rem x s)) 1:perm_eq_sym 2:rem_uniq.
+proof.
+  move=> ^ /perm_eqP_pred1 + /perm_eq_mem + /count_uniq_mem => eqcnt eqin cntin. 
+  by apply count_mem_uniq => x; rewrite -(eqcnt x) -(eqin x) (cntin x).
 qed.
 
 lemma perm_eq_uniq (s1 s2 : 'a list) :
   perm_eq s1 s2 => uniq s1 <=> uniq s2.
-proof. by move => ^ /perm_eq_sym /perm_eq_uniq_impl + /perm_eq_uniq_impl. qed.
+proof. by move=> ^ /perm_eq_sym /perm_eq_uniq_impl + /perm_eq_uniq_impl. qed.
 
 lemma leq_size_uniq (s1 s2 : 'a list):
   uniq s1 => (mem s1 <= mem s2) => size s2 <= size s1 => uniq s2.