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