---

Step * of Lemma per-function_wf_type

∀[A:Type]. (per-function(A;a.Type) ∈ 𝕌')
BY
{ (Intros
   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].  (per-function(A;a.Type)  \mmember{}  \mBbbU{}')


By

---

Latex:
(Intros
  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