Read-only archive. Publishing has closed. GitHub
theorem BFO.NonSpatialIndependentContinuant.mk.inj
theorem BFO.NonSpatialIndependentContinuant.mk.inj
: ∀ {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 ·

View source in hz46pbq2

Definitional, with no premises to accept.