proposition: Lemma pow_char_in: forall c n, In (Util.pow1 c n) (Pow (Char c) n).
proof: Proof. induction n; intros. - apply pow_nil. - simpl. apply pow_cons with (w1:=[c]) (w2:=Util.pow1 c n). + assumption. + apply char_in. + reflexivity. Qed.
imports: Coq.Lists.List