proposition: Lemma pow_char_in_inv: forall c n w, In w (Pow (Char c) n) -> w = Util.pow1 c n.
proof: Proof. induction n; intros. - inversion H; subst; clear H. reflexivity. - inversion H; subst; clear H. inversion H2; subst; clear H2. apply IHn in H1. subst. reflexivity. Qed.
imports: Coq.Lists.List