---

Step * of Lemma per-apply_wf

∀[A:Type]. ∀[B:type-function{i:l}(A)]. ∀[f:per-function(A;a.B[a])]. ∀[a:A].  (per-apply(f;a) ∈ tf-apply(B;a))
BY
{ (RepeatFor 3 (Intro⋅) THEN InstLemma `per-function_wf` [⌜A⌝;⌜B⌝]⋅ THEN 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
⊢ per-apply(f;a) ∈ tf-apply(B;a)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:type-function\{i:l\}(A)].  \mforall{}[f:per-function(A;a.B[a])].  \mforall{}[a:A].
    (per-apply(f;a)  \mmember{}  tf-apply(B;a))


By

---

Latex:
(RepeatFor  3  (Intro\mcdot{})  THEN  InstLemma  `per-function\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index