The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 25 Apr 2011 18:08:51 +0200 (CEST),
Marko Maliković 
<marko AT ffri.hr>
 a écrit :

> 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ć
> 

Your question is not clear, but your first case is rather a proof of
"(forall A, A) -> goal" (which is trivial to prove, just apply H), and
the second is rather a proof of "forall A, A -> goal" (which may be
non trivial or even false, depending on "goal").

So, as the things to prove are different, I guess that knowing if the
proofs are equivalent has no real meaning.

What is equivalent is rather:
"
A: Prop
H: A
==============
goal
",
"
A: Prop
==============
forall (H:A) -> goal
" and
"
==============
forall (A:Prop) (H:A) -> goal
"
but I guess you already know it