---

Step * of Lemma cbv-intro-test

∀[T:Type]. ∀x:T. T supposing value-type(T)
BY
{ (BasicUniformUnivCD Auto⋅ THEN (cbvAllIntro THENA Auto)) }

1
.....aux..... 
1. [T] : Type
2. [%] : value-type(T)
3. x : T
⊢ value-type(T)

2
1. [T] : Type
2. [%] : value-type(T)
3. x : T
⊢ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  T  supposing  value-type(T)


By

---

Latex:
(BasicUniformUnivCD  Auto\mcdot{}  THEN  (cbvAllIntro  THENA  Auto))

---

Home Index