proposition: Lemma pow_pow_in_inv_eq: forall c1 c2 n1 n2 m1 m2, c1 <> c2 -> App (Pow (Char c1) n1) (Pow (Char c2) n2) (Util.pow1 c1 m1 ++ Util.pow1 c2 m2) -> n1 = m1 /\ n2 = m2.
proof: Proof. intros. apply pow_pow_in_inv in H0. assert (n1 = m1) by eauto using Util.pow1_app_inv_eq_1. subst. assert (n2 = m2) by eauto using Util.pow1_app_inv_eq_2. subst. intuition. Qed.
imports: Coq.Lists.List