proposition: Lemma pow_succ_equiv: forall n L1 L2, L1 == L2 -> L1 ^^ n == L2 ^^ n -> L1 ^^ S n == L2 ^^ S n.
proof: Proof. split; intros. - inversion H1; subst; clear H1. apply H0 in H3. apply pow_cons with (w1:=w1) (w2:=w2); auto. apply H in H4. assumption. - inversion H1; subst; clear H1. apply H0 in H3. apply pow_cons with (w1:=w1) (w2:=w2); auto. apply H in H4. assumption. Qed.
imports: Coq.Lists.List