Step * of Lemma cbv-intro-test

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

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

2
1. [T] Type
2. [%] value-type(T)
3. 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