---

Step * of Lemma type-function_wf

∀[A:Type]. (type-function{i:l}(A) ∈ 𝕌')
BY
{ (Auto
   THEN Unfold `type-function` 0
   THEN InstLemma `per-function_wf_base_family` [⌜parm{i'}⌝;⌜A⌝;⌜λ2a.Type⌝]⋅
   THEN Auto
   THEN D 0
   THEN RepUR ``so_lambda`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  (type-function\{i:l\}(A)  \mmember{}  \mBbbU{}')


By

---

Latex:
(Auto
  THEN  Unfold  `type-function`  0
  THEN  InstLemma  `per-function\_wf\_base\_family`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a.Type\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  RepUR  ``so\_lambda``  0
  THEN  Auto)

---

Home Index