The Coq mailing list

[Victor Porton <porton AT narod.ru>]

We should be able to take a proof of a true proposition. Is it implemented in 
Coq 8.3.pl2? My native attempt to do this steps on an error.

[[[[
Parameter P: Prop.

Axiom P_true: P.

Theorem t: True.
proof.
  let X be such that (X : P).
end proof. Qed.
]]]]

Error: In environment
X : P
The term "X:P" has type "P" which should be Set, Prop or Type.

I hope Coq allows to get around this, but I'm not sure.

-- 
Victor Porton - http://portonvictor.org