theorem MurderCase.mk.inj
theorem MurderCase.mk.inj
: ∀ {murder : t8grzs37.Murder} {murderer victim : t8grzs37.Person} {punishment : t8grzs37.PunishmentSpecification}
  {murders_in : t8grzs37.MurdersIn (Subtype.val murderer) (Subtype.val victim) (Subtype.val murder)}
  {deserved_punishment :
    t8grzs37.DeservesPunishmentFor (Subtype.val murderer) (Subtype.val murder) (Subtype.val punishment)}
  {murder_1 : t8grzs37.Murder} {murderer_1 victim_1 : t8grzs37.Person} {punishment_1 : t8grzs37.PunishmentSpecification}
  {murders_in_1 : t8grzs37.MurdersIn (Subtype.val murderer_1) (Subtype.val victim_1) (Subtype.val murder_1)}
  {deserved_punishment_1 :
    t8grzs37.DeservesPunishmentFor (Subtype.val murderer_1) (Subtype.val murder_1) (Subtype.val punishment_1)},
  t8grzs37.MurderCase.mk murder murderer victim punishment murders_in deserved_punishment =
      t8grzs37.MurderCase.mk murder_1 murderer_1 victim_1 punishment_1 murders_in_1 deserved_punishment_1 →
    murder = murder_1 ∧ murderer = murderer_1 ∧ victim = victim_1 ∧ punishment = punishment_1