Extracted Smaller Locale instantiation into its own lemma.