proposition: Lemma pow1_app_inv_eq_1: forall {T} (a b:T), a <> b -> forall x y v w, pow1 a x ++ pow1 b y = pow1 a v ++ pow1 b w -> x = v.
proof: Proof. intros ? a b. induction x; intros. { simpl in *. destruct v; auto. destruct y; simpl in *; inversion H0; subst; clear H0. contradiction. } simpl in *. destruct v; simpl in *. { destruct w; inversion H0; subst; clear H0. contradiction. } inversion H0; subst; clear H0. apply IHx in H2. subst; reflexivity. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List