proposition: Lemma set_to_listK m (X: {set 'I_m}) : (list_to_set m (char_seq X)) = X.
proof: Proof. by apply/setP => i; rewrite inE char_seq_prop (@val_inj _ _ _ (Ordinal (ltn_ord i)) i). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)