proposition: Lemma pow1_app_inv_eq_2: forall {T} (a:T) w y z, w ++ pow1 a y = w ++ pow1 a z -> y = z.
proof: Proof. intros. apply app_inv_eq_l in H. apply pow1_inv_eq in H. assumption. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List