∀ {«notation» recommendedSpelling : String} {additionalInformation? : Option String}
  {notation_1 recommendedSpelling_1 : String} {additionalInformation?_1 : Option String},
  { «notation» := «notation», recommendedSpelling := recommendedSpelling,
        additionalInformation? := additionalInformation? } =
      { «notation» := notation_1, recommendedSpelling := recommendedSpelling_1,
        additionalInformation? := additionalInformation?_1 } →
    «notation» = notation_1 ∧
      recommendedSpelling = recommendedSpelling_1 ∧ additionalInformation? = additionalInformation?_1