proposition: Lemma itr'_level n (x: expr n n): e_level (itr' x) ≪ STR+e_level x.
proof: Proof. unfold itr'. case is_zer_spec. reflexivity. case is_top_spec. solve_lower'. cbn. now rewrite remove_level. Qed.
imports: kleene syntax powerfix