---

Step * 1 1 of Lemma uncurry-gen_wf


1. B : Type
2. d : ℕ
3. ∀d:ℕd. ∀n,m:ℕ.
     ((m ≤ n)
     ⇒ ((n - m) ≤ d)
     ⇒ (∀A:ℕn ⟶ Type. ∀g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B).
           (uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)))
4. n : ℕ
5. m : ℕ
6. (m + 1) ≤ n
7. (n - m) ≤ d
8. A : ℕn ⟶ Type
9. g : (k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)
10. ∀n,m:ℕ.
      ((m ≤ n)
      ⇒ ((n - m) ≤ (d - 1))
      ⇒ (∀A:ℕn ⟶ Type. ∀g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B).
            (uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)))
11. x : k:ℕn ⟶ (A k)
12. v : funtype(n - m;λx.(A (x + m));B)
13. (g x) = v ∈ funtype(n - m;λx.(A (x + m));B)
⊢ v (x m) ∈ funtype(n - m + 1;λx.(A (x + m + 1));B)
BY
{ (Thin (-1)
   THEN (RWO "funtype-unroll" (-1) THENA Auto')
   THEN Reduce (-1)
   THEN SplitOnHypITE -1 
   THEN Auto'
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  Type
2.  d  :  \mBbbN{}
3.  \mforall{}d:\mBbbN{}d.  \mforall{}n,m:\mBbbN{}.
          ((m  \mleq{}  n)
          {}\mRightarrow{}  ((n  -  m)  \mleq{}  d)
          {}\mRightarrow{}  (\mforall{}A:\mBbbN{}n  {}\mrightarrow{}  Type.  \mforall{}g:(k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B).
                      (uncurry-gen(n)  m  g  \mmember{}  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  B)))
4.  n  :  \mBbbN{}
5.  m  :  \mBbbN{}
6.  (m  +  1)  \mleq{}  n
7.  (n  -  m)  \mleq{}  d
8.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
9.  g  :  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)
10.  \mforall{}n,m:\mBbbN{}.
            ((m  \mleq{}  n)
            {}\mRightarrow{}  ((n  -  m)  \mleq{}  (d  -  1))
            {}\mRightarrow{}  (\mforall{}A:\mBbbN{}n  {}\mrightarrow{}  Type.  \mforall{}g:(k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B).
                        (uncurry-gen(n)  m  g  \mmember{}  (k:\mBbbN{}n  {}\mrightarrow{}  (A  k))  {}\mrightarrow{}  B)))
11.  x  :  k:\mBbbN{}n  {}\mrightarrow{}  (A  k)
12.  v  :  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)
13.  (g  x)  =  v
\mvdash{}  v  (x  m)  \mmember{}  funtype(n  -  m  +  1;\mlambda{}x.(A  (x  +  m  +  1));B)


By

---

Latex:
(Thin  (-1)
  THEN  (RWO  "funtype-unroll"  (-1)  THENA  Auto')
  THEN  Reduce  (-1)
  THEN  SplitOnHypITE  -1 
  THEN  Auto'
  THEN  DoSubsume
  THEN  Auto)

---

Home Index