---

Step * 2 of Lemma funtype-split


1. k : ℤ
2. 0 < k
3. ∀T:Type. ∀m:ℤ.
     ((0 ≤ m)
     ⇒ (∀A:ℕm + (k - 1) ⟶ Type. (funtype(m + (k - 1);A;T) = funtype(m;A;funtype(k - 1;λk.(A (k + m));T)) ∈ Type)))
4. T : Type
5. m : ℤ
6. 0 ≤ m
7. A : ℕm + k ⟶ Type
⊢ funtype(m + k;A;T) = funtype(m;A;funtype(k;λk.(A (k + m));T)) ∈ Type
BY
{ ((RW (AddrC [2] (LemmaC `funtype-unroll-last-eq`)) 0 THENA Auto)
   THEN AutoSplit
   THEN Try (Complete (Auto'))
   THEN (RW (AddrC [3;3] (LemmaC `funtype-unroll-last-eq`)) 0 THENA Auto)
   THEN AutoSplit
   THEN (Subst ⌜(m + k) - 1 ~ m + (k - 1)⌝ 0⋅ THENA Auto)
   THEN (Subst ⌜(k - 1) + m ~ m + (k - 1)⌝ 0⋅ THENA Auto)
   THEN BackThruSomeHyp
   THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}T:Type.  \mforall{}m:\mBbbZ{}.
          ((0  \mleq{}  m)
          {}\mRightarrow{}  (\mforall{}A:\mBbbN{}m  +  (k  -  1)  {}\mrightarrow{}  Type
                      (funtype(m  +  (k  -  1);A;T)  =  funtype(m;A;funtype(k  -  1;\mlambda{}k.(A  (k  +  m));T)))))
4.  T  :  Type
5.  m  :  \mBbbZ{}
6.  0  \mleq{}  m
7.  A  :  \mBbbN{}m  +  k  {}\mrightarrow{}  Type
\mvdash{}  funtype(m  +  k;A;T)  =  funtype(m;A;funtype(k;\mlambda{}k.(A  (k  +  m));T))


By

---

Latex:
((RW  (AddrC  [2]  (LemmaC  `funtype-unroll-last-eq`))  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Try  (Complete  (Auto'))
  THEN  (RW  (AddrC  [3;3]  (LemmaC  `funtype-unroll-last-eq`))  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (Subst  \mkleeneopen{}(m  +  k)  -  1  \msim{}  m  +  (k  -  1)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(k  -  1)  +  m  \msim{}  m  +  (k  -  1)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto')

---

Home Index