proposition: Lemma pow_char_cons_inv: forall c n w, In w (Pow (Char c) (S n)) -> exists w', w = c::w' /\ In w' (Pow (Char c) n).
proof: Proof. intros. inversion H; subst; clear H. inversion H2; subst; clear H2. exists w2. auto. Qed.
imports: Coq.Lists.List