proposition: Lemma pow_in_eq: forall (L:language) w, In w L -> In w (Pow L 1).
proof: Proof. intros. apply pow_cons with (w1:=w) (w2:=nil). + apply pow_nil. + assumption. + rewrite app_nil_r. reflexivity. Qed.
imports: Coq.Lists.List