型健全性というと type preservation と progress が成り立ってればよいというのがよくある話ですが，それでなぜ健全といえるのかというところをわざわざ形式的に書いてみた話です。といっても，わかりやすい説明をしようという気はあまりなくて，知ってる人…