∀ {α : Type} {«private» «public» private_1 public_1 : α},
  { «private» := «private», «public» := «public» } = { «private» := private_1, «public» := public_1 } →
    «private» = private_1 ∧ «public» = public_1