proposition: Lemma pow_char_cons: forall c n w, In w (Pow (Char c) n) -> In (c::w) (Pow (Char c) (S n)).
proof: Proof. intros. apply pow_cons with (w1:=[c]) (w2:=w). - assumption. - apply char_in. - reflexivity. Qed.
imports: Coq.Lists.List