---

Step * of Lemma very-dep-fun-eta

No Annotations
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])].  (f = (λL,b. (f L b)) ∈ very-dep-fun(A;B;a,b.C[a;b]\000C))
BY
{ (Auto
   THEN All (Unfold `very-dep-fun`)
   THEN (Enough to prove ∀n:ℕ. (f = (λL,b. (f L b)) ∈ vdf(A;B;a,b.C[a;b];n))
          Because (EqTypeCD
                   THEN Auto
                   THEN ((Decide ⌜0 ≤ n⌝⋅ THENA Auto)
                         THENL [((D -3 With ⌜n⌝  THENA Auto) THEN D -4 With ⌜n⌝  THEN Auto)
                               ; ((D -4 With ⌜n⌝  THENA Auto)
                                  THEN (Unfold `vdf` -1 THEN (OReduce (-1) THENA Auto))
                                  THEN Unfold `vdf` 0
                                  THEN OReduce 0
                                  THEN Auto
                                  THEN GenConcl ⌜f = F ∈ ({L:(a:A × b:B × C[a;b]) List| ||L|| = 0 ∈ ℤ}  ⟶ B ⟶ A)⌝⋅
                                  THEN Auto)]
                   )))) }

1
1. A : Type
2. B : Type
3. C : A ⟶ B ⟶ Type
4. f : ⋂n:ℤ. vdf(A;B;a,b.C[a;b];n)
⊢ ∀n:ℕ. (f = (λL,b. (f L b)) ∈ vdf(A;B;a,b.C[a;b];n))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type].  \mforall{}[f:very-dep-fun(A;B;a,b.C[a;b])].    (f  =  (\mlambda{}L,b.  (f  L  b)))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `very-dep-fun`)
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}.  (f  =  (\mlambda{}L,b.  (f  L  b)))
                Because  (EqTypeCD
                                  THEN  Auto
                                  THEN  ((Decide  \mkleeneopen{}0  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                                              THENL  [((D  -3  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)  THEN  D  -4  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto)
                                                          ;  ((D  -4  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)
                                                                THEN  (Unfold  `vdf`  -1  THEN  (OReduce  (-1)  THENA  Auto))
                                                                THEN  Unfold  `vdf`  0
                                                                THEN  OReduce  0
                                                                THEN  Auto
                                                                THEN  GenConcl  \mkleeneopen{}f  =  F\mkleeneclose{}\mcdot{}
                                                                THEN  Auto)]
                                  ))))

---

Home Index