proposition: Lemma accept_pow1: forall c i, pow1 c i \in r_star (r_char c).
proof: Proof. induction i. - apply accept_star_nil. - simpl. apply accept_star_cons with (s1:=[c]) (s2:=pow1 c i). + apply accept_char. + assumption. + reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang