theorem CapabilityRoute.mk.injEq
theorem CapabilityRoute.mk.injEq
: ∀ (sourceNodeId recipientNodeId capabilityId recipientInterfaceId contextUnits : Nat)
  (interfaceCompatible sufficientContext provenancePresent localValidationPassed : Bool)
  (recipientCorrectionWork validatedUses validatedReuseCount sourceNodeId_1 recipientNodeId_1 capabilityId_1
    recipientInterfaceId_1 contextUnits_1 : Nat)
  (interfaceCompatible_1 sufficientContext_1 provenancePresent_1 localValidationPassed_1 : Bool)
  (recipientCorrectionWork_1 validatedUses_1 validatedReuseCount_1 : Nat),
  (e50am64c.CapabilityRoute.mk sourceNodeId recipientNodeId capabilityId recipientInterfaceId contextUnits
        interfaceCompatible sufficientContext provenancePresent localValidationPassed recipientCorrectionWork
        validatedUses validatedReuseCount =
      e50am64c.CapabilityRoute.mk sourceNodeId_1 recipientNodeId_1 capabilityId_1 recipientInterfaceId_1 contextUnits_1
        interfaceCompatible_1 sufficientContext_1 provenancePresent_1 localValidationPassed_1 recipientCorrectionWork_1
        validatedUses_1 validatedReuseCount_1) =
    (sourceNodeId = sourceNodeId_1 ∧
      recipientNodeId = recipientNodeId_1 ∧
        capabilityId = capabilityId_1 ∧
          recipientInterfaceId = recipientInterfaceId_1 ∧
            contextUnits = contextUnits_1 ∧
              interfaceCompatible = interfaceCompatible_1 ∧
                sufficientContext = sufficientContext_1 ∧
                  provenancePresent = provenancePresent_1 ∧
                    localValidationPassed = localValidationPassed_1 ∧
                      recipientCorrectionWork = recipientCorrectionWork_1 ∧
                        validatedUses = validatedUses_1 ∧ validatedReuseCount = validatedReuseCount_1)