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!