The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am attempting to rewrite equality of dependent records in C-zar style. 
Below is a partial proof:

[[[[
Record Foo := {
  a : nat;
  b : a > 0
}.

Theorem thm (u v : Foo) : (a u = a v -> u = v).
proof.
  assume (a u = a v).
  have ((a u > 0) = (a v > 0)).
  have (a u > 0).
  then ( (b u) : (a u > 0) ).
end proof. Qed.
]]]]

This produces the error:

Toplevel input, characters 7-24:
Error: In environment
u : Foo
v : Foo
_fact0 : a u > 0
The term "b u:a u > 0" has type "a u > 0" which should be Set, Prop or Type.

I wonder why it does not work. We know that [b u] is a proof of [a u > 0] 
what is a true proposition and therefore [b u] is of the type [a u > 0].

I wonder how to circumvent this error. Why is it limited to only Set, Prop or 
Type?

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