theorem instFiatObjectPartAtToParent
theorem instFiatObjectPartAtToParent: ∀ (x t : Type) [FiatObjectPart.At x t], MaterialEntity.At x t
theorem instFiatObjectPartAtToParent
theorem instFiatObjectPartAtToParent: ∀ (x t : Type) [FiatObjectPart.At x t], MaterialEntity.At x t