proposition: Lemma nil_pow_in_inv: forall n w, In w (Pow Nil n) -> w = [].
proof: Proof. induction n; intros. - inversion H; subst; clear H. reflexivity. - inversion H; subst; clear H. apply nil_in_inv in H2. subst. apply IHn in H1. subst. reflexivity. Qed.
imports: Coq.Lists.List