proposition: Lemma l3_spec: L3 == fun w => exists w', ["a"] ++ w' ++ ["b"] = w.
proof: Proof. unfold L3; split; intros. - apply app_r_char_in_inv in H. destruct H as (w1, (?, Hw)). apply app_l_char_in_inv in Hw. destruct Hw as (w2, (?, _)). subst. simpl. exists w2. reflexivity. - unfold In in H. destruct H as (w', ?). subst. simpl. apply app_assoc_in_1. apply app_l_char_in. apply app_l_all_in. apply char_in. Qed.
imports: Coq.Lists.List