∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : p → l ⊕ m),
  (Matrix.fromBlocks A B C D).submatrix Sum.swap f = (Matrix.fromBlocks C D A B).submatrix id f