theorem instImmaterialEntityAtToParent
theorem instImmaterialEntityAtToParent
: ∀ (x t : Type) [ImmaterialEntity.At x t], IndependentContinuant.At x t