This is a placeholder milestone that groups together work needed to implement simple static checking of bounds declarations. By simple, we mean checking that relies no normalization, syntactic equality, and facts about variable equality.