sig
val
eq_refl :
Term
.types
->
Term
.constr
->
Term
.constr
val
eq :
Term
.types
->
Term
.constr
end