added discussion of Leibniz equality
added discussion of lifted primitive and Leibniz equality
submission version for Archive of Formal proofs