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

View source in j12bzjgj

Definitional, with no premises to accept.