---

Step * of Lemma mk_lambdas-fun_wf

∀[T,U:Type]. ∀[m:ℕ]. ∀[n:ℕm + 1]. ∀[A:ℕm ⟶ Type]. ∀[F:(funtype(m;A;T) ⟶ T) ⟶ U].
∀[G:∀[T:Type]. (funtype(n;A;T) ⟶ T)].
  (mk_lambdas-fun(F;G;n;m) ∈ funtype(m - n;λi.(A (i + n));U))
BY
{ (Auto'
   THEN RepeatFor 2 ((D (-4) THENA Auto))
   THEN (Assert ⌜∃j:ℕ. (m = (n + j) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
   THEN D (-1)
   THEN RepeatFor 2 (MoveToConcl (-4))
   THEN HypSubst' (-1) 0
   THEN ThinVar `m'
   THEN (Subst ⌜(n + j) - n ~ j⌝ 0⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)) }

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

2
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)

---

Latex:

---

Latex:
\mforall{}[T,U:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].  \mforall{}[A:\mBbbN{}m  {}\mrightarrow{}  Type].  \mforall{}[F:(funtype(m;A;T)  {}\mrightarrow{}  T)  {}\mrightarrow{}  U].
\mforall{}[G:\mforall{}[T:Type].  (funtype(n;A;T)  {}\mrightarrow{}  T)].
    (mk\_lambdas-fun(F;G;n;m)  \mmember{}  funtype(m  -  n;\mlambda{}i.(A  (i  +  n));U))


By

---

Latex:
(Auto'
  THEN  RepeatFor  2  ((D  (-4)  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}\mexists{}j:\mBbbN{}.  (m  =  (n  +  j))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  D  (-1)
  THEN  RepeatFor  2  (MoveToConcl  (-4))
  THEN  HypSubst'  (-1)  0
  THEN  ThinVar  `m'
  THEN  (Subst  \mkleeneopen{}(n  +  j)  -  n  \msim{}  j\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto))

---

Home Index