The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

On 09/05/2010 08:00, Patrice Chalin wrote:
> I would like to do a forall elimination on H. While in general I know that 
> this
> is impossible (because T might not be inhabited), in this case, we have the
> witness x : T.        Hence, I would like to be able to instantiate H with 
> x. Can
> this be done in Coq?

There are various ways to do that ; you may use the following tactics
and their variants :

specialize (H x).

(* This one will keep the name H for the specialize hypothesis, or : *)

assert (H' := H x).

(* You need to pick up a fresh name for this one. *)

PMP

Attachment: signature.asc
Description: OpenPGP digital signature