theorem RelationNamedState.mk.injEq
theorem RelationNamedState.mk.injEq
: ∀ (params iparams : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (args : Array (Lean.TSyntax `ident))
  (conjuncts : Array (Lean.Name × Lean.TSyntax `term)) (nextInst : Nat)
  (params_1 iparams_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (args_1 : Array (Lean.TSyntax `ident))
  (conjuncts_1 : Array (Lean.Name × Lean.TSyntax `term)) (nextInst_1 : Nat),
  (a52pkb71.RelationNamedState.mk params iparams args conjuncts nextInst =
      a52pkb71.RelationNamedState.mk params_1 iparams_1 args_1 conjuncts_1 nextInst_1) =
    (params = params_1 ∧ iparams = iparams_1 ∧ args = args_1 ∧ conjuncts = conjuncts_1 ∧ nextInst = nextInst_1)