unfold mapMIdx
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ mapMIdx f empty = pure empty
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ mapMIdx.loop f empty 0 (_ : 0 ≤ 0) (mkEmpty 0) = pure empty