---

Step * 1 of Lemma sq_stable__has-value


1. A : Type
2. value-type(A)
3. a : bar(A)
⊢ SqStable((a)↓)
BY
{ D 0 }

1
1. A : Type
2. value-type(A)
3. a : bar(A)
4. ↓(a)↓
⊢ (a)↓

2
.....wf..... 
1. A : Type
2. value-type(A)
3. a : bar(A)
⊢ ↓(a)↓ ∈ ℙ

---

Latex:

---

Latex:

1.  A  :  Type
2.  value-type(A)
3.  a  :  bar(A)
\mvdash{}  SqStable((a)\mdownarrow{})


By

---

Latex:
D  0

---

Home Index