うお。Coq の Calculus of (Co)Inductive Constructions って subject reduction 満たさないのか。 しかもそんな理由で。

まあ、依存型の型理論では subject reduction は簡単そうに見えて、結構他の性質と衝突したりするので、そこまで驚きではないけれど。