---

Step * of Lemma function-valueall-type

∀[A:Type]. ∀[B:A ⟶ Type].  valueall-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 (Assert ¬(⊥)↓ BY
               Auto)
   THEN RecUnfold `evalall` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (HVimplies  0 [1])
   THEN RW (SweepUpC StuckApplyC) 7
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    valueall-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  (Assert  \mneg{}(\mbot{})\mdownarrow{}  BY
                          Auto)
  THEN  RecUnfold  `evalall`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (HVimplies    0  [1])
  THEN  RW  (SweepUpC  StuckApplyC)  7
  THEN  Auto)

---

Home Index