title: How to read ∀x.(p(x)⇒∀y.p(y))?
body: <p>In a question I asked here: <a href="https://stackoverflow.com/questions/38417547/px%E2%87%92%E2%88%80x-px-is-contingent/38417592#38417592">p(x)⇒∀x.p(x) is contingent?</a>
  It seems that there's tendency to agree upon  p(x)⇒∀x.p(x) is the same as ∀x.(p(x)⇒∀y.p(y)), whereas ∀x.(p(x)⇒∀y.p(y)) is read as if p(x) is true for <strong>some</strong> x, then it is true for all x.</p>
  
  <p>However I don't understand where's the quantifier <strong>SOME</strong> came from, since there no quantifier '∃' in '∀x.(p(x)⇒∀y.p(y))'</p>
  
  <p>Is there any sort of quantifier distribution law makes the quantifier changed in the ∀x.(p(x)⇒∀y.p(y)) ?</p>