∀ {α : Type u_1} (m n : ℕ),
  Fin.appendEquiv m n =
    { toFun := fun fg => Fin.append fg.1 fg.2,
      invFun := fun f => (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i)), left_inv := ⋯, right_inv := ⋯ }