The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Thu, Jun 23, 2011 at 06:30:43PM +0200, gallais @ ensl.org wrote:
> Hi Georgi,
> 
> Your [Theorem T : Prop] proves that [Prop] is inhabited while
> your [Axiom A : T] states that [T] is inhabited.
> 
> These statements are not equivalent.
> 
> Cheers,
>

Thank you.

Do you mean that if I take theorems as axioms it doesn't matter
what the theorem states (Prop in this case) but how it is proved?

-- 
joro