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

Published by @sam ·

View source in z2yhb66n

Definitional, with no premises to accept.