---

Step * of Lemma cbva-intro-test

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index