proposition: Lemma r_pow_char_in_inv: forall n c w, w \in r_pow (r_char c) n -> w = pow1 c n.
proof: Proof. induction n; intros. - inversion H; subst; clear H. reflexivity. - inversion H; subst; clear H. apply IHn in H3. subst. inversion H2; subst; clear H2. reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang