theorem instPunishmentSpecificationAtToParent
theorem instPunishmentSpecificationAtToParent
: ∀ (x t : Type) [PunishmentSpecification.At x t], GenericallyDependentContinuant.At x t