Read-only archive. Publishing has closed. GitHub
theorem VictimIsChild.eq_1
theorem VictimIsChild.eq_1
: ∀ (mc : etsbfws7.MurderCase),
  etsbfws7.VictimIsChild mc =
    ∃ t,
      z69f3rb3.Child.At (Subtype.val (etsbfws7.MurderCase.victim mc)) t ∧
        hz46pbq2.BFO.ProcessOccupiesTemporalRegion (Subtype.val (etsbfws7.MurderCase.murder mc)) t

Published by @sam ·

View source in etsbfws7

Definitional, with no premises to accept.