theorem instRealizableEntityAtToParent
theorem instRealizableEntityAtToParent
: ∀ (x t : Type) [RealizableEntity.At x t], SpecificallyDependentContinuant.At x t