proposition: Lemma map_enc_inj {s t} : map enc s = map enc t -> s = t.
proof: Proof. elim: s t; first by case. move=> ? ? IH [|? ?]; first done. by move=> /= [/enc_inj -> /IH ->]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun