---

Step * 1 1 2 of Lemma gen_hyp_tp

.....assertion..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
⊢ e ∈ A
BY
{ (Thin (-1) THEN AddHiddenLabel `wf`) }

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

---

Latex:

---

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


By

---

Latex:
(Thin  (-1)  THEN  AddHiddenLabel  `wf`)

---

Home Index