The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

Damien Pous' goal was not provable ("B true" and "B false" are
distinct types of same cardinality and they can be interpreted by the
same set in a model).

This one is a variant of Hofmann-Streicher's Uniqueness of Reflexive
Identity Proofs (UIP_refl) and it is probably equivalent to it. It
requires one of the (weak) axioms equivalent to UIP_refl, e.g. JMeq_eq
from file JMeq.v or eq_rect_eq in Eqdep.v.

Require Import JMeq.
Inductive B: bool -> Set := ff: B false | tt: B true. 
Goal forall (x : bool) (b : B x), b = (if x as x0 return (B x0) then tt else 
ff).
intros x b.
apply JMeq_eq.
assert (H:x=x) by reflexivity.
destruct x in H at 1 |- * at 2 3; 
  destruct b; discriminate || reflexivity.
Qed.

The third line may need some Set Printing All (or some Maj-Alt-A or
whatever binding you have for that in CoqIDE) to know how to number
occurrences.

Hugo