---

Step * 2 of Lemma mk_lambdas-fun_wf


1. T : Type
2. U : Type
3. j : ℤ
4. 0 < j
5. ∀n:ℤ
     ((0 ≤ n)
     ⇒ (∀A:ℕn + (j - 1) ⟶ Type. ∀G:∀[T:Type]. (funtype(n;A;T) ⟶ T). ∀F:(funtype(n + (j - 1);A;T) ⟶ T) ⟶ U.
           (mk_lambdas-fun(F;G;n;n + (j - 1)) ∈ funtype(j - 1;λi.(A (i + n));U))))
6. n : ℤ
7. 0 ≤ n
8. A : ℕn + j ⟶ Type
9. G : ∀[T:Type]. (funtype(n;A;T) ⟶ T)
10. F : (funtype(n + j;A;T) ⟶ T) ⟶ U
⊢ mk_lambdas-fun(F;G;n;n + j) ∈ funtype(j;λi.(A (i + n));U)
BY
{ (RecUnfold `mk_lambdas-fun` 0
   THEN (BoolCase ⌜n + j ≤z n⌝⋅ THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))) }

1
1. T : Type
2. U : Type
3. j : ℤ
4. 0 < j
5. ∀n:ℤ
     ((0 ≤ n)
     ⇒ (∀A:ℕn + (j - 1) ⟶ Type. ∀G:∀[T:Type]. (funtype(n;A;T) ⟶ T). ∀F:(funtype(n + (j - 1);A;T) ⟶ T) ⟶ U.
           (mk_lambdas-fun(F;G;n;n + (j - 1)) ∈ funtype(j - 1;λi.(A (i + n));U))))
6. n : ℤ
7. ¬((n + j) ≤ n)
8. 0 ≤ n
9. A : ℕn + j ⟶ Type
10. G : ∀[T:Type]. (funtype(n;A;T) ⟶ T)
11. F : (funtype(n + j;A;T) ⟶ T) ⟶ U
⊢ λx.mk_lambdas-fun(F;λf.(G f x);n + 1;n + j) ∈ funtype(j;λi.(A (i + n));U)

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  \mforall{}n:\mBbbZ{}
          ((0  \mleq{}  n)
          {}\mRightarrow{}  (\mforall{}A:\mBbbN{}n  +  (j  -  1)  {}\mrightarrow{}  Type.  \mforall{}G:\mforall{}[T:Type].  (funtype(n;A;T)  {}\mrightarrow{}  T).
                  \mforall{}F:(funtype(n  +  (j  -  1);A;T)  {}\mrightarrow{}  T)  {}\mrightarrow{}  U.
                      (mk\_lambdas-fun(F;G;n;n  +  (j  -  1))  \mmember{}  funtype(j  -  1;\mlambda{}i.(A  (i  +  n));U))))
6.  n  :  \mBbbZ{}
7.  0  \mleq{}  n
8.  A  :  \mBbbN{}n  +  j  {}\mrightarrow{}  Type
9.  G  :  \mforall{}[T:Type].  (funtype(n;A;T)  {}\mrightarrow{}  T)
10.  F  :  (funtype(n  +  j;A;T)  {}\mrightarrow{}  T)  {}\mrightarrow{}  U
\mvdash{}  mk\_lambdas-fun(F;G;n;n  +  j)  \mmember{}  funtype(j;\mlambda{}i.(A  (i  +  n));U)


By

---

Latex:
(RecUnfold  `mk\_lambdas-fun`  0
  THEN  (BoolCase  \mkleeneopen{}n  +  j  \mleq{}z  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))))

---

Home Index