∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} (f : α → β) (e₁ : l → m)
  (e₂ : o → n) (A : Matrix m n α), (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f