theorem instObjectAggregateAtToParent
theorem instObjectAggregateAtToParent: ∀ (x t : Type) [ObjectAggregate.At x t], MaterialEntity.At x t
theorem instObjectAggregateAtToParent
theorem instObjectAggregateAtToParent: ∀ (x t : Type) [ObjectAggregate.At x t], MaterialEntity.At x t