Module conv 

Definitional equality of values: Lean’s algorithm, in the classic engine’s order of attempts.

Quick structural cases and proven pairs first; the ≡ true shortcut; whnf_core without unfolding projections’ structures; proof irrelevance; lazy δ-reduction by definitional height (comparing two applications of the same definition argument by argument, skipping the positions its definition cannot distinguish, before unfolding either); then constants, variables and projections; full whnf_core; congruence of applications; η; struct-η; string literals; unit-like types. A β-step is an environment extension, a δ-step a remembered unfolding, and a binder is crossed by applying both closures to one fresh variable.

Proven pairs are closed under congruence but not transitivity: Lean’s definitional equality is not transitive (proof irrelevance), see the classic engine’s ProvenEqual.