---

Step * of Lemma mk_lambdas_wf

∀[T:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ Type]. ∀[F:T].  (mk_lambdas(F;m) ∈ funtype(m;A;T))
BY
{ (Auto
   THEN Unfold `mk_lambdas` 0
   THEN NatInd (-3)
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN RepUR ``funtype`` 0
   THEN Try (Complete (Auto))
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN (MemCD THENA Auto)
   THEN Unfold `funtype` (-3)
   THEN (InstHyp [⌜λi.(A (i + 1))⌝] (-3)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[A:\mBbbN{}m  {}\mrightarrow{}  Type].  \mforall{}[F:T].    (mk\_lambdas(F;m)  \mmember{}  funtype(m;A;T))


By

---

Latex:
(Auto
  THEN  Unfold  `mk\_lambdas`  0
  THEN  NatInd  (-3)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``funtype``  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (MemCD  THENA  Auto)
  THEN  Unfold  `funtype`  (-3)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.(A  (i  +  1))\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  DoSubsume
  THEN  Auto)

---

Home Index