The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

A bit of follow-up (not essential to understand my previous post):

Since the two worlds, namely the completeness proof and the necessity
of the algebraic laws, which are for the application of the logic, do
not interact, I have Set-valued logic for the completeness and
Prop-valued one for using the logic.  Two logics have exactly the same
rules, but I cannot prove them equivalent, of course. I thought that
it would be nicer if I can merge them.

Keiko