---

Step * of Lemma function-value-type

∀[A:Type]. ∀[B:A ⟶ Type].  value-type(a:A ⟶ B[a]) supposing ↓∃a:A. value-type(B[a])
BY
{ (Auto
   THEN D -1
   THEN Unhide
   THEN Auto
   THEN ExRepD
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RenameVar `f' (-2)
   THEN (Assert (f a)↓ BY
               Auto)
   THEN HasValueD (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    value-type(a:A  {}\mrightarrow{}  B[a])  supposing  \mdownarrow{}\mexists{}a:A.  value-type(B[a])


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Unhide
  THEN  Auto
  THEN  ExRepD
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RenameVar  `f'  (-2)
  THEN  (Assert  (f  a)\mdownarrow{}  BY
                          Auto)
  THEN  HasValueD  (-1)
  THEN  Auto)

---

Home Index