proposition: Lemma pow_add_inv: forall L n1 n2 (w:word), In w (Pow L (n1 + n2)) -> exists w1 w2, w = w1 ++ w2 /\ In w1 (Pow L n1) /\ In w2 (Pow L n2).
proof: Proof. induction n1; simpl; intros. { exists nil, w. intuition. apply pow_nil. } inversion H; subst; clear H. assert (Hx := H1). apply IHn1 in H1. destruct H1 as (w3, (w4, (?, (Ha, Hb)))). subst. exists (w1 ++ w3) % list, w4. rewrite app_assoc. intuition. unfold In. eauto using pow_cons. Qed.
imports: Coq.Lists.List