∀ {n : ℕ} {σ : Type u_1} {τ : Type u_2} [inst : DecidableEq σ] [inst_1 : DecidableEq τ] (μ : n.Partition) (e : σ ≃ τ),
  Function.RightInverse (fun x => ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) fun x => ⟨(Sym.equivCongr e) ↑x, ⋯⟩