Set Default Goal Selector $"!".$

Require Import Coq.Strings.Ascii.

Require Import Coq.Lists.List.

From Turing Require Import Lang.

From Turing Require Import Util.

Import LangNotations.

Import ListNotations.

Import Lang.Examples.

Open Scope lang$\_$scope.

Open Scope char$\_$scope.

$(*---------------------------------------------------------------------------*)$

$(**$

Show that any word that is in L$4$ is either empty or starts with $"$a$".$

$*)$

Theorem ex$1$:

forall w$,$ L$4$ w $->$ w $=[]\backslash /$ exists w$\text{'},$ w $="$a$"$ :: w$\text{'}.$

Proof.