theorem BFO.NonSpatialIndependentContinuant.mk.injEq

theorem BFO.NonSpatialIndependentContinuant.mk.injEq
theorem BFO.NonSpatialIndependentContinuant.mk.injEq
: ∀ (val : hz46pbq2.BFO.IndependentContinuant)
  (not_spatial_at : ∀ (t : hz46pbq2.BFO.Time), ¬hz46pbq2.BFO.SpatialRegion.At (Subtype.val val) (Subtype.val t))
  (val_1 : hz46pbq2.BFO.IndependentContinuant)
  (not_spatial_at_1 : ∀ (t : hz46pbq2.BFO.Time), ¬hz46pbq2.BFO.SpatialRegion.At (Subtype.val val_1) (Subtype.val t)),
  (hz46pbq2.BFO.NonSpatialIndependentContinuant.mk val not_spatial_at =
      hz46pbq2.BFO.NonSpatialIndependentContinuant.mk val_1 not_spatial_at_1) =
    (val = val_1)

Published by @sam · Jul 3, 2026

View source in hz46pbq2

Definitional, with no premises to accept.