proposition: Lemma star_inv_cons: forall r c w, c :: w \in r_star r -> exists w1 w2, w1 ++ w2 = w /\ c :: w1 \in r /\ w2 \in r_star r.
proof: Proof. intros. inversion H; subst. destruct s1. { contradiction. } simpl in *. inversion H3; subst; clear H3. eauto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang