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