UIP in Lean source code

Stream: lean4

[Chris Henson]

I've seen mentioned before that Lean has UIP as an "axiom" (quotes because I'm not sure if it literally uses axiom). I searched for a bit and couldn't find it, could someone point me to where in the source code that is? Thanks!

[Henrik Böving]

It's integrated into the implementation of type checking through the fact that you can proof two proofs of the same proposition are the same by rfl. There is no explicit axiom.