theorem RelationNamedState.mk.injEq
theorem RelationNamedState.mk.injEq
: ∀ (params : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (args : Array (Lean.TSyntax `ident))
  (insts : Array (Lean.TSyntax `Lean.Parser.Command.structInstBinder)) (nextInst : Nat)
  (params_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (args_1 : Array (Lean.TSyntax `ident))
  (insts_1 : Array (Lean.TSyntax `Lean.Parser.Command.structInstBinder)) (nextInst_1 : Nat),
  (va6mxd60.RelationNamedState.mk params args insts nextInst =
      va6mxd60.RelationNamedState.mk params_1 args_1 insts_1 nextInst_1) =
    (params = params_1 ∧ args = args_1 ∧ insts = insts_1 ∧ nextInst = nextInst_1)