∀ (ref : Lean.Syntax) (idx : ℕ) (ref_1 : Lean.Syntax) (idx_1 : ℕ),
  (Lean.Elab.Term.StructInst.FieldLHS.fieldIndex ref idx = Lean.Elab.Term.StructInst.FieldLHS.fieldIndex ref_1 idx_1) =
    (ref = ref_1 ∧ idx = idx_1)