theorem BFO.NonSpatialIndependentContinuant.mk.sizeOf_spec

theorem BFO.NonSpatialIndependentContinuant.mk.sizeOf_spec
theorem BFO.NonSpatialIndependentContinuant.mk.sizeOf_spec
: ∀ (val : j12bzjgj.BFO.IndependentContinuant)
  (not_spatial_at : ∀ (t : j12bzjgj.BFO.Time), ¬j12bzjgj.BFO.SpatialRegion.At (Subtype.val val) (Subtype.val t)),
  sizeOf (j12bzjgj.BFO.NonSpatialIndependentContinuant.mk val not_spatial_at) = 1 + sizeOf val

Published by @sam · Jul 4, 2026

View source in j12bzjgj

Definitional, with no premises to accept.