The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>]

Patrice Chalin wrote:
> Abstractly speaking, while constructing a proof, I have reached the following
> situation
>
>   x : T
>   H : forall x' : T, P x'
>   ...
>   ============================
>    G
>
> for some complex term P : T -> Prop. Assume that G can no longer me worked on.
> 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?
>
>   
If you want a forall elimination

assert (H1 := H x).

will do the job.

--
Laurent