The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 01/09/2013 04:45 PM, Andrew Hirsch wrote:
> I have a couple of lemmas about the standard Coq library I would like
> to be able to use in a project. However, I can't find a proof of
> either, and it seems that there isn't one in the standard libraries.
>
> The first is about Sigma types. I want to prove that:
> forall (A : Set) (Q : A ->  Prop) (b : {a : A | Q a}), b = exist Q
> (proj1_sig b) (proj2_sig b).
>    

This looks like it could be proved by [destruct b; reflexivity].

> With this decision procedure:
> Definition var_eq : forall (a b  : var), {a = b} + {a<>  b}.
> [...]
>
> I want to then prove:
> forall (x : var) (A : Set) (a b : A), (if var_dec x x then a else b) = a.
>    

The decision procedure implementation doesn't matter.  You can do 
[intros; destruct (var_dec x x); tauto], which follows just from the 
_type_ of the procedure.