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. cbn. rewrite itr_pls_itr, pls'pls by (rewrite 2remove_level; solve_lower'). rewrite <-(IHx1 eq_refl), <-(IHx2 eq_refl) by solve_lower'. simpl cast. apply itr_pls_itr. - now rewrite 2cast_eq, itr_invol. Qed.
imports: kleene syntax powerfix