The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Hello all,

Perhaps the following question is naive but I do not find a solution:

Is it possible context, which contains a hypothesis with dependent
product, for example:

H : forall A : Prop, A
============================
 goal

into the context with quantifier free hypothesis:

A : Prop
H : A
============================
 goal

Are the above two proofs equivalent at all?

Thanx and greetings,

Marko Malikoviæ