theorem MurderCase.mk.sizeOf_spec
theorem MurderCase.mk.sizeOf_spec
: ∀ (murder : xxzf15qm.Murder) (murderer victim : xxzf15qm.Person) (punishment : xxzf15qm.PunishmentSpecification)
  (murders_in : xxzf15qm.MurdersIn (Subtype.val murderer) (Subtype.val victim) (Subtype.val murder))
  (deserved_punishment :
    xxzf15qm.DeservesPunishmentFor (Subtype.val murderer) (Subtype.val murder) (Subtype.val punishment)),
  sizeOf (xxzf15qm.MurderCase.mk murder murderer victim punishment murders_in deserved_punishment) =
    1 + sizeOf murder + sizeOf murderer + sizeOf victim + sizeOf punishment + sizeOf murders_in +
      sizeOf deserved_punishment