proposition: Lemma pow_add: forall L n1 n2 (w1 w2:word), In w1 (Pow L n1) -> In w2 (Pow L n2) -> In (w1 ++ w2) (Pow L (n1 + n2)).
proof: Proof. induction n1; intros. - inversion H; subst; clear H; simpl. assumption. - inversion H; subst; clear H. simpl. assert (Hx := IHn1 _ _ _ H2 H0). rewrite <- app_assoc. eapply pow_cons; eauto. Qed.
imports: Coq.Lists.List