cases hi
case empty
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : Fin (size #[]) → α → β
i : Nat
hi : i < size (mapIdx #[] f)
⊢ (mapIdx #[] f)[i] = f { val := i, isLt := (_ : i < size #[]) } #[][i]
no goals