proposition: Lemma itr'itr l n (x: expr n n) {Hl: STR+e_level x ≪ l}: itr' x ==_[l] x^+.
proof: Proof. symmetry. unfold itr'. revert Hl. case is_zer_spec. intros. apply itr0. case is_top_spec. intros. apply itrtop. intros. symmetry. now apply remove_spec. Qed.
imports: kleene syntax powerfix