theorem Example.child_case_deserves_greater_punishment
theorem Example.child_case_deserves_greater_punishment
(logic_is_actual : LogicIsActual)
(principle : A ChildMurderDeservesGreaterPunishmentThanNonChildMurder)
(cases : A TwoConcreteMurderCases)
: A (IsGreaterPunishmentThan
      ChildCasePunishmentSpec
      AdultCasePunishmentSpec)