theorem SameNonVictimAgeCircumstances.eq_1

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

Published by @sam · Jul 3, 2026

View source in etsbfws7

Definitional, with no premises to accept.