fact: Fixpoint as_lang r := match r with | r_void => Void | r_nil => Nil | r_char c => Char c | r_app r1 r2 => App (as_lang r1) (as_lang r2) | r_union r1 r2 => Union (as_lang r1) (as_lang r2) | r_star r => Star (as_lang r) end.
imports: Coq.micromega.Lia Turing.Util Turing.Lang