---

Step * of Lemma mk_applies_wf

∀[T:Type]. ∀[m,n:ℕ]. ∀[A:ℕm + n ⟶ Type]. ∀[G:k:ℕm ⟶ (A k)]. ∀[F:funtype(m + n;A;T)].
  (mk_applies(F;G;m) ∈ funtype(n;λk.(A (m + k));T))
BY
{ (BasicUniformUnivCD Auto'
   THEN Unhide
   THEN MoveToConcl 3
   THEN NatInd 2
   THEN Reduce 0
   THEN (UnivCD THENA Auto')⋅
   THEN Try (Complete (((Subst ⌜0 + n ~ n⌝ (-1)⋅ THENA Auto)
                        THEN RepUR ``mk_applies`` 0
                        THEN Auto
                        THEN DoSubsume
                        THEN Auto
                        THEN Subst ⌜(λk.(A (0 + k))) = A ∈ (ℕn ⟶ Type)⌝ 0⋅
                        THEN Auto
                        THEN Ext
                        THEN Reduce 0
                        THEN Auto)))
   THEN RepUR ``mk_applies`` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Fold `mk_applies` 0) }

1
1. T : Type
2. m : ℤ
3. m ≠ 0
4. 0 < m
5. ∀n:ℕ. ∀A:ℕ(m - 1) + n ⟶ Type. ∀G:k:ℕm - 1 ⟶ (A k). ∀F:funtype((m - 1) + n;A;T).
     (mk_applies(F;G;m - 1) ∈ funtype(n;λk.(A ((m - 1) + k));T))
6. n : ℕ
7. A : ℕm + n ⟶ Type
8. G : k:ℕm ⟶ (A k)
9. F : funtype(m + n;A;T)
⊢ mk_applies(F;G;m - 1) (G (m - 1)) ∈ funtype(n;λk.(A (m + k));T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m,n:\mBbbN{}].  \mforall{}[A:\mBbbN{}m  +  n  {}\mrightarrow{}  Type].  \mforall{}[G:k:\mBbbN{}m  {}\mrightarrow{}  (A  k)].  \mforall{}[F:funtype(m  +  n;A;T)].
    (mk\_applies(F;G;m)  \mmember{}  funtype(n;\mlambda{}k.(A  (m  +  k));T))


By

---

Latex:
(BasicUniformUnivCD  Auto'
  THEN  Unhide
  THEN  MoveToConcl  3
  THEN  NatInd  2
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto')\mcdot{}
  THEN  Try  (Complete  (((Subst  \mkleeneopen{}0  +  n  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                                            THEN  RepUR  ``mk\_applies``  0
                                            THEN  Auto
                                            THEN  DoSubsume
                                            THEN  Auto
                                            THEN  Subst  \mkleeneopen{}(\mlambda{}k.(A  (0  +  k)))  =  A\mkleeneclose{}  0\mcdot{}
                                            THEN  Auto
                                            THEN  Ext
                                            THEN  Reduce  0
                                            THEN  Auto)))
  THEN  RepUR  ``mk\_applies``  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Fold  `mk\_applies`  0)

---

Home Index