Precise reference for the equivalence of $E_n$ algebras and locally constant factorization algebra? I've seen the following theorem attributed to Lurie:

Theorem. There is an equivalence of $(\infty,1)$-categories between $E_n$ algebras and locally constant factorization algebra on $\mathbf{R}^n$.

And the reference is usually given as Lurie's Higher Algebra. However it's a 1500+ pages book and search for "factorization algebra" doesn't have a match. 
Can anyone give me a pointer to where exactly this is proved in Higher Algebra, or in some other books? Thanks.
 A: The result in question is a corollary to proposition 5.4.5.15 in Higher Algebra

Theorem 5.4.5.9. Let $M$ be a manifold and let $C^⊗$ be an $∞$-operad. Composition with the map
  $$\mathrm{Disk}(M)^⊗ → \mathbb{E}_M^⊗$$
  of Remark 5.4.5.8 induces a fully faithful embedding
  $$θ:\mathrm{Alg}_{\mathbb{E}_M}(C) → \mathrm{Alg}_{\mathrm{Disk}(M)}(C)\,.$$
  The essential image of $θ$ is the full subcategory of $\mathrm{Alg}_{\mathrm{Disk}(M)}(C)$ spanned by the locally constant $\mathrm{Disk}(M)^⊗$-algebra objects of $C$.

When $M=\mathbb{R}^n$, the $\infty$-operad $\mathbb{E}_M$  is just the $\mathbb{E}_n$-operad.
Be careful that the book does not use the language of factorization algebras, but if you compare the definitions you'll see that there is a conservative functor from locally constant factorization algebras on $M$ to locally constant $\mathrm{Disk}(M)$-algebras such that the functor in theorem 5.4.5.9 factors as
$$\mathrm{Alg}_{\mathbb{E}_M}(C)→\mathrm{Fact}^{lc}_M(C)→\mathrm{Alg}_{\mathrm{Disk}(M)}(C)$$
where the middle term is the $\infty$-category of locally constant factorization algebras and the first arrow is the one given by taking factorization homology. This, plus the existence of the "global sections" functor $\mathrm{Fact}^{lc}_M(C)→\mathrm{Alg}_{\mathbb{E}_M}(C)$ is enough to conclude the result you're after.
