theorem BFO.NonSpatialIndependentContinuant.mk.sizeOf_spec

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

Published by @sam · Jul 3, 2026

View source in hz46pbq2

Definitional, with no premises to accept.