---

Step * of Lemma apply-nth_wf

∀[T:Type]. ∀[n:ℕ]. ∀[A:ℕn + 1 ⟶ Type]. ∀[f:funtype(n + 1;A;T)]. ∀[x:A[n]].  (apply-nth(n; f; x) ∈ funtype(n;A;T))
BY
{ xxx(Auto
      THEN Unfold `apply-nth` 0
      THEN GenConclAtAddrType ⌜funtype(n + 1;A;T) ⟶ funtype(n;A;T)⌝[2;1]⋅
      THEN Try (Complete (Auto))
      THEN All Thin)xxx }

1
1. T : Type
2. n : ℕ
3. A : ℕn + 1 ⟶ Type
4. x : A[n]
⊢ primrec(n;λf.(f x);λi,H,f. (H o f)) ∈ funtype(n + 1;A;T) ⟶ funtype(n;A;T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  +  1  {}\mrightarrow{}  Type].  \mforall{}[f:funtype(n  +  1;A;T)].  \mforall{}[x:A[n]].
    (apply-nth(n;  f;  x)  \mmember{}  funtype(n;A;T))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `apply-nth`  0
        THEN  GenConclAtAddrType  \mkleeneopen{}funtype(n  +  1;A;T)  {}\mrightarrow{}  funtype(n;A;T)\mkleeneclose{}[2;1]\mcdot{}
        THEN  Try  (Complete  (Auto))
        THEN  All  Thin)xxx

---

Home Index