The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/06/2016 12:29 PM, Jonathan Leivent wrote:
> On 09/06/2016 12:12 PM, Matthieu Sozeau wrote:
> > ...
> > In effect, this would be what the definitional version of uniqueness of
> > identity proofs (aka the K rule/axiom) would give you, i.e. it would use
> > type information to convert plus_n_Sm 0 1 : S (0 + 1) = 0 + S 1 to 
> > eq_refl
> > : 2 = 2. This rule is not part of Coq's type theory (and neither from
> > standard Martin-Löf Type Theory).
>
> But, you can use Eqdep_dec.UIP_refl_nat to rewrite those match 
> discriminees down to eq_refl.
>
> -- Jonathan

Which is a little more difficult than I expected, but this works:

Require Import Eqdep_dec.
Goal True.
pose (vector_rev Example2_01 (nil bool)) as v.
compute in v.
pose proof (eq_refl:v=v) as E.
unfold v in E at 1.
repeat rewrite (ltac:(apply UIP_refl_nat)) in E.

-- Jonathan