proposition: Lemma pow_equiv: forall (L1 L2:language), Equiv L1 L2 -> forall n, Equiv (Pow L1 n) (Pow L2 n).
proof: Proof. split; intros. + eauto using pow_equiv_in. + apply equiv_sym in H. eauto using pow_equiv_in. Qed.
imports: Coq.Lists.List