proposition: Lemma l4_spec: L4 == fun x => exists n, pow1 "a" n ++ pow1 "b" n = x.
proof: Proof. unfold L4; split; intros. - destruct H as (n, Hw). exists n. apply app_in_inv in Hw. destruct Hw as (w1, (w2, (?, (Ha, Hb)))). subst. apply pow_char_in_inv in Ha. apply pow_char_in_inv in Hb. subst. reflexivity. - destruct H as (n, H). subst. exists n. apply app_in_eq. + apply pow_char_in. + apply pow_char_in. Qed.
imports: Coq.Lists.List