---

Step * 1 1 of Lemma per-apply_wf


1. A : Type
2. B : type-function{i:l}(A)
3. f : per-function(A;a.B[a])
4. per-function(A;a.B[a]) ∈ Type
5. a : A
6. f[a] ∈ B[a]
⊢ per-apply(f;a) ∈ tf-apply(B;a)
BY
{ (All (Unfolds ``so_apply per-apply tf-apply``) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  type-function\{i:l\}(A)
3.  f  :  per-function(A;a.B[a])
4.  per-function(A;a.B[a])  \mmember{}  Type
5.  a  :  A
6.  f[a]  \mmember{}  B[a]
\mvdash{}  per-apply(f;a)  \mmember{}  tf-apply(B;a)


By

---

Latex:
(All  (Unfolds  ``so\_apply  per-apply  tf-apply``)  THEN  Auto)

---

Home Index