theorem
proved
phiUniformClosedLevels_eq_original_of_uniform_growth_seed
show as:
phiUniformClosedLevels_eq_original_of_uniform_growth_seed