proposition: Lemma occurrences_pow1: forall c n, occurrences c (pow1 c n) = n.
proof: Proof. induction n; intros; simpl. - reflexivity. - rewrite Ascii.eqb_refl. rewrite IHn. reflexivity. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List