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