proposition: Lemma remove_spec_dep' l n m (x: expr n m): forall (H: n=m) {Hl: STR+e_level x ≪ l}, (cast H eq_refl (remove x))^* ==_[l] (cast H eq_refl x)^*.
proof: Proof. induction x; cbn; trivial; intros H Hl. - subst. simpl cast. rewrite str_pls_str. rewrite <-(IHx1 eq_refl), <-(IHx2 eq_refl) by solve_lower'. simpl cast. rewrite <-str_pls_str. apply str_weq. apply pls'pls. rewrite 2remove_level; solve_lower'. - rewrite 2cast_eq. apply antisym. apply str_leq. apply itr_ext. apply str_ind_l1. apply str_refl. now rewrite itr_str_l, str_cons, str_trans. Qed.
imports: kleene syntax powerfix