Irrelevance, Heterogeneous Equality, and Call-by-Value Dependent Type Systems