theorem RelationNamedState.mk.inj

theorem RelationNamedState.mk.inj
theorem RelationNamedState.mk.inj
: ∀ {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

Published by @sam · Jul 3, 2026

View source in va6mxd60

Definitional, with no premises to accept.