---

Step * of Lemma partial_ap_wf

∀[T:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[g:funtype(n;A;T) ⟶ T].  (partial_ap(g;n;m) ∈ funtype(m;A;T) ⟶ T)
BY
{ (ProveWfLemma
   THEN (InstLemma `funtype-split` [⌜T⌝;⌜n⌝;⌜m⌝;⌜A⌝]⋅ THENA Auto)
   THEN (Assert ⌜mk_lambdas_fun(λh.mk_lambdas(h f;n - m);m) ∈ funtype(m;A;funtype(n - m;λk.(A (k + m));T))⌝⋅ THENM Auto)
   THEN Using [`T',⌜T⌝] (BLemma `mk_lambdas_fun_wf`)⋅
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[g:funtype(n;A;T)  {}\mrightarrow{}  T].
    (partial\_ap(g;n;m)  \mmember{}  funtype(m;A;T)  {}\mrightarrow{}  T)


By

---

Latex:
(ProveWfLemma
  THEN  (InstLemma  `funtype-split`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}mk\_lambdas\_fun(\mlambda{}h.mk\_lambdas(h  f;n  -  m);m)  \mmember{}  funtype(m;A;funtype(n 
                              -  m;\mlambda{}k.(A  (k  +  m));T))\mkleeneclose{}\mcdot{}
  THENM  Auto
  )
  THEN  Using  [`T',\mkleeneopen{}T\mkleeneclose{}]  (BLemma  `mk\_lambdas\_fun\_wf`)\mcdot{}
  THEN  Auto')

---

Home Index