no goals
α : Type ?u.44179
β : Type ?u.44182
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l
rw [raise, lower, add_tsub_cancel_right, lower_raise l]