Theorem provers based on dependent types rely on efficient full-reducers implementing a beta-equivalence tester for their typing rules. We present a full-reducing strategy in a strict calculus allowing open terms. We traverse a path, starting at weak-reduction in a non-strict calculus restricted to closed terms (call-by-name). By successively strengthening the congruence rules (reducing under lambda abstractions), assuring normalisation (resorting to hybrid strategies to find a normal form, if it exists), restricting the notion of reduction (allowing only values as arguments) and generalizing the set of legal terms (including open terms) we get a normalizing strategy in Plotkin’s lambda_V theory. We show how these four different aspects (strengthening congruence, normalisation, by-value semantics and open terms) are entangled in this traversal. Meta-theoretic issues regarding standardisation and confluence lead the way to full-reduction.