theorem SameNonVictimAgeCircumstances.eq_1

theorem SameNonVictimAgeCircumstances.eq_1
theorem SameNonVictimAgeCircumstances.eq_1
: ∀ (mc1 mc2 : z2yhb66n.MurderCase),
  z2yhb66n.SameNonVictimAgeCircumstances mc1 mc2 =
    (z2yhb66n.MurderCircumstancesRelevantToTheDeservedPunishmentOtherThanVictimAge
        (Subtype.val (z2yhb66n.MurderCase.murder mc1)) ↔
      z2yhb66n.MurderCircumstancesRelevantToTheDeservedPunishmentOtherThanVictimAge
        (Subtype.val (z2yhb66n.MurderCase.murder mc2)))

Published by @sam · Jul 4, 2026

View source in z2yhb66n

Definitional, with no premises to accept.