Read-only archive. Publishing has closed. GitHub
theorem RelationSlotSpec.mk.injEq
theorem RelationSlotSpec.mk.injEq
: ∀ (binderTy rawTy : Lean.TSyntax `term) (constraint? : Option (Lean.TSyntax `ident))
  (binderTy_1 rawTy_1 : Lean.TSyntax `term) (constraint?_1 : Option (Lean.TSyntax `ident)),
  (r59jf3ak.RelationSlotSpec.mk binderTy rawTy constraint? =
      r59jf3ak.RelationSlotSpec.mk binderTy_1 rawTy_1 constraint?_1) =
    (binderTy = binderTy_1 ∧ rawTy = rawTy_1 ∧ constraint? = constraint?_1)

Published by @sam ·

View source in r59jf3ak

Definitional, with no premises to accept.