theorem MurderCase.mk.injEq
theorem MurderCase.mk.injEq
: ∀ (murder : z2yhb66n.Murder) (murderer victim : mw1nngvh.Person) (punishment : z2yhb66n.PunishmentSpec)
  (murders_involvement : z2yhb66n.MurderInvolves (Subtype.val murder) (Subtype.val victim) (Subtype.val murderer))
  (deserved_punishment :
    z2yhb66n.DeservesPunishmentFor (Subtype.val murderer) (Subtype.val punishment) (Subtype.val murder))
  (murder_1 : z2yhb66n.Murder) (murderer_1 victim_1 : mw1nngvh.Person) (punishment_1 : z2yhb66n.PunishmentSpec)
  (murders_involvement_1 :
    z2yhb66n.MurderInvolves (Subtype.val murder_1) (Subtype.val victim_1) (Subtype.val murderer_1))
  (deserved_punishment_1 :
    z2yhb66n.DeservesPunishmentFor (Subtype.val murderer_1) (Subtype.val punishment_1) (Subtype.val murder_1)),
  (z2yhb66n.MurderCase.mk murder murderer victim punishment murders_involvement deserved_punishment =
      z2yhb66n.MurderCase.mk murder_1 murderer_1 victim_1 punishment_1 murders_involvement_1 deserved_punishment_1) =
    (murder = murder_1 ∧ murderer = murderer_1 ∧ victim = victim_1 ∧ punishment = punishment_1)