The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gyesik Lee wrote:
> Sorry, a bit late in the discussion.
>
>    
> > There are two main options.  First, you can use a cast:
> >
> > Hypothesis t_full :
> >   forall n:nat, exists s:States, match t_nat in _ = T return T with
> > refl_equal =>  s t end = n.
> >      
> I really like this "case" trick. But I am really wondering if we can
> avoid using  [JMeq] in principle or at least in many (how many?)
> cases?
>    

I can answer "yes" if you're OK with this statement of the property: 
[JMeq] with its associated axiom is logically/expressively equivalent to 
normal equality with the [eq_rect_eq] axiom from Coq's [Eqdep] library.  
Chapter 9 of CPDT (http://adam.chlipala.net/cpdt/) shows how to encode 
each predicate and its introduction/elimination rules in terms of the 
other predicate and its rules.