# Assumption Rule in Dependent Type Theories

I am reading an introductory book on type theory and formal proof, I get confused with the assumption rule:

If $$\Gamma\vdash A: Type$$ and if $$x\not\in FV(\Gamma)$$, then $$\Gamma, x:A\vdash x:A$$.

My questions are:

(1) If $$y:A\rightarrow\perp$$ is an assumption in $$\Gamma$$, then does $$\Gamma$$ derives $$A:Type$$?

(2) If (1) is the case, shall we extend $$\Gamma$$ with the new assumption $$x: A$$?

I think there must be some clearer explanation for the conditions of application of the assumption rule, but it is at least not clear from the introductory book I am reading. Thanks!