fact: Fixpoint is_clean n m (x: expr n m) := match x with | e_one _ | e_var _ => True | e_pls x y | e_dot x y => is_clean x /\ is_clean y | e_cnv x | e_itr x | e_str x => is_clean x | _ => False end.
imports: kleene syntax