theorem CapabilityRoute.mk.inj
theorem CapabilityRoute.mk.inj
: ∀ {sourceNodeId recipientNodeId capabilityId recipientInterfaceId contextUnits : Nat}
  {provenancePresent localValidationPassed : Bool}
  {recipientCorrectionWork validatedUses sourceNodeId_1 recipientNodeId_1 capabilityId_1 recipientInterfaceId_1
    contextUnits_1 : Nat}
  {provenancePresent_1 localValidationPassed_1 : Bool} {recipientCorrectionWork_1 validatedUses_1 : Nat},
  g1fbxjjj.CapabilityRoute.mk sourceNodeId recipientNodeId capabilityId recipientInterfaceId contextUnits
        provenancePresent localValidationPassed recipientCorrectionWork validatedUses =
      g1fbxjjj.CapabilityRoute.mk sourceNodeId_1 recipientNodeId_1 capabilityId_1 recipientInterfaceId_1 contextUnits_1
        provenancePresent_1 localValidationPassed_1 recipientCorrectionWork_1 validatedUses_1 →
    sourceNodeId = sourceNodeId_1 ∧
      recipientNodeId = recipientNodeId_1 ∧
        capabilityId = capabilityId_1 ∧
          recipientInterfaceId = recipientInterfaceId_1 ∧
            contextUnits = contextUnits_1 ∧
              provenancePresent = provenancePresent_1 ∧
                localValidationPassed = localValidationPassed_1 ∧
                  recipientCorrectionWork = recipientCorrectionWork_1 ∧ validatedUses = validatedUses_1