[STATEMENT]
lemma \<P>\<^sub>1_pow: "blinfun_apply (\<P>\<^sub>1 ^^ n) = blinfun_apply \<P>\<^sub>1 ^^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (\<P>\<^sub>1 ^^ n) = blinfun_apply \<P>\<^sub>1 ^^ n
[PROOF STEP]
by (induction n) auto