proposition: Lemma pow_equiv_in: forall L1 L2 n w, Equiv L1 L2 -> In w (Pow L1 n) -> In w (Pow L2 n).
proof: Proof. intros. induction H0; intros. - apply pow_nil. - subst. apply pow_cons with (w1:=w1) (w2:=w2); auto. apply H. assumption. Qed.
imports: Coq.Lists.List