proposition: Lemma repeat_a0 {n} : repeat 0 n = map enc (repeat a0 n).
proof: Proof. elim: n; first done. move=> n /= ->. congr cons. rewrite /enc. by case: (sym_eq_dec a0 a0). Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun