proposition: Lemma pow1_a_b_inv_eq: 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 /\ y = w.
proof: Proof. intros. assert (Hx := H0). apply pow1_app_inv_eq_1 in H0; auto. subst. apply app_inv_eq_l in Hx. apply pow1_inv_eq in Hx. auto. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List