Equality is reflexive by construction: this is the proof that a value
equals itself, named so library code can pass it around.
328def stdEqualReflexive =
329 (lambda erased element : Type 0 . (lambda unrestricted value : element . (refl element value)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.