定理

正しく型付けされた項が評価できるなら、評価後の項も正しく型付けされている

証明