theorem instDispositionAtToParent
theorem instDispositionAtToParent: ∀ (x t : Type) [Disposition.At x t], RealizableEntity.At x t
theorem instDispositionAtToParent
theorem instDispositionAtToParent: ∀ (x t : Type) [Disposition.At x t], RealizableEntity.At x t