---

Step * 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
⊢ per-apply(f;a) ∈ tf-apply(B;a)
BY
{ (InstLemma `apply-wf-per` [⌜A⌝;⌜B⌝;⌜f⌝;⌜a⌝]⋅ THENA Auto) }

1
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)

---

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
\mvdash{}  per-apply(f;a)  \mmember{}  tf-apply(B;a)


By

---

Latex:
(InstLemma  `apply-wf-per`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index