---

Step * 1 1 1 of Lemma gen_hyp_tp

.....assertion..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
⊢ A ∈ Type
BY
{ AddHiddenLabel `wf` }

1
.....wf..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
⊢ A ∈ Type

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  e  :  A
3.  H  :  A  {}\mrightarrow{}  \mBbbU{}\{j\}
4.  z  :  H  e
\mvdash{}  A  \mmember{}  Type


By

---

Latex:
AddHiddenLabel  `wf`

---

Home Index