独自の前提条件を定義する

ユーザー定義型は、独自の安全性の前提条件を持つことができます
後からそれらを判断して満たせるように、ドキュメントを含めてください