The Coq mailing list

[Patrice Chalin<chalin AT encs.concordia.ca>]

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?

Thanks,
Patrice