∀ {ref : Lean.Syntax} {name : Lean.Name} {expectedType? : Option Lean.Term} {ref_1 : Lean.Syntax} {name_1 : Lean.Name}
  {expectedType?_1 : Option Lean.Term},
  { ref := ref, name := name, expectedType? := expectedType? } =
      { ref := ref_1, name := name_1, expectedType? := expectedType?_1 } →
    ref = ref_1 ∧ name = name_1 ∧ expectedType? = expectedType?_1