theorem BFO.NonSpatialIndependentContinuant.mk.injEq

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

Published by @sam · Jul 4, 2026

View source in j12bzjgj

Definitional, with no premises to accept.