∀ {kind : Lean.SyntaxNodeKind} {a : Lean.TSyntax kind} {kind_1 : Lean.SyntaxNodeKind} {a_1 : Lean.TSyntax kind_1},
  Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a = Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a_1 →
    kind = kind_1 ∧ a ≍ a_1