Равноиндексированные индуктивные типы подразумевают равные индексы
Давайте fooиндексировать индуктивный тип x : X. Parameter X : Type. Inductive foo : X -> Type := | constr : forall (x : X), foo x. Мне любопытно, если foo x = foo yподразумевается x = y. У меня нет идей, как это доказать. Lemma type_equality_implies_index_equality : forall (x y : X), foo x = foo...