∀ (toSnapshot : Lean.Language.Snapshot) (cmdState : Lean.Elab.Command.State) (toSnapshot_1 : Lean.Language.Snapshot)
  (cmdState_1 : Lean.Elab.Command.State),
  ({ toSnapshot := toSnapshot, cmdState := cmdState } = { toSnapshot := toSnapshot_1, cmdState := cmdState_1 }) =
    (toSnapshot = toSnapshot_1 ∧ cmdState = cmdState_1)