fact: Fixpoint clean n m (x: expr n m): expr n m := match x with | e_zer _ _ => 0 | e_one _ => 1 | e_pls x y => e_pls' (clean x) (clean y) | e_dot x y => e_dot' (clean x) (clean y) | e_itr x => e_itr' (clean x) | e_str x => e_str' (clean x) | e_cnv x => e_cnv' (clean x) | e_var a => e_var a | x => x end%ast.
imports: kleene syntax