fix and prove: Definitions of uniq, Lemma 'count_uniq_mem'
generate htmls using coqdoc
fix proof