хитрое сопоставление с образцом без аксиом

Question

Предположим, у меня есть следующий тип:

Inductive foo : Type -> Type :=
  | A : forall X, Empty_set -> foo X
  | B : foo unit.

Могу ли я доказать следующее:

Lemma obv : forall x : foo unit, x = B.

без аксиом? Тактика dependent destruction позаботится об этом довольно легко, но это вводит аксиому JMeq_eq. Я нашел эту статью, но в данном случае она не применима, поскольку Type не имеет UIP.

Answer 1

Нет, это невозможно доказать без чего-то вроде однолистности или UIP. Тип foo unit изоморфен типу unit = unit, поэтому доказательство того, что все жители foo unit равны B, равнозначно доказательству того, что все жители unit = unit равны eq_refl, и это не может быть доказано без аксиом, в Coq.