---

Step * 1 of Lemma tf-apply_wf


1. [A] : Type
2. [a] : A
3. [B] : per-function(A;a.Type)
⊢ B a ∈ Type
BY
{ (Unhide
   THEN PointwiseFunctionality 3
   THEN Try (Unhide)
   THEN Try ((EqCD THEN Auto))
   THEN At ⌜𝕌'⌝ (PerHD (-1))⋅
   THEN Try (Complete ((At ⌜𝕌'⌝ UniverseIsType⋅ THEN (BLemma `function-eq_wf` THEN Auto) THEN D 0 THEN Auto)))
   THEN TACTIC:InstLemma `function-eq-implies` [⌜parm{i'}⌝]⋅
   THEN (FHyp (-1) [-2] THEN Auto)
   THEN Try (Complete ((InstHyp [⌜a⌝] (-1)⋅ THEN Auto)))
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [a]  :  A
3.  [B]  :  per-function(A;a.Type)
\mvdash{}  B  a  \mmember{}  Type


By

---

Latex:
(Unhide
  THEN  PointwiseFunctionality  3
  THEN  Try  (Unhide)
  THEN  Try  ((EqCD  THEN  Auto))
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (PerHD  (-1))\mcdot{}
  THEN  Try  (Complete  ((At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  UniverseIsType\mcdot{}
                                            THEN  (BLemma  `function-eq\_wf`  THEN  Auto)
                                            THEN  D  0
                                            THEN  Auto)))
  THEN  TACTIC:InstLemma  `function-eq-implies`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
  THEN  (FHyp  (-1)  [-2]  THEN  Auto)
  THEN  Try  (Complete  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)))
  THEN  D  0
  THEN  Auto)

---

Home Index