---

Step * of Lemma base-member-per-function

∀[A:Type]. ∀[B:per-function(A;x.Type)]. ∀[f:Base].
  f ∈ per-function(A;x.B[x]) supposing ∀[a,a':Base].  (f a) = (f a') ∈ B[a] supposing a = a' ∈ A
BY
{ (Intro
   THEN (InstLemma `per-function_wf_type` [⌜A⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (Intro)
   THEN (InstLemma `per-function-type-apply` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (InstLemma `per-function_wf` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN Intro) }

1
1. [A] : Type
2. per-function(A;a.Type) ∈ 𝕌'
3. [B] : per-function(A;x.Type)
4. [f] : Base
5. ∀[a:A]. (B[a] ∈ Type)
6. per-function(A;a.B[a]) ∈ Type
7. [%7] : ∀[a,a':Base].  (f a) = (f a') ∈ B[a] supposing a = a' ∈ A
⊢ f ∈ per-function(A;x.B[x])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:per-function(A;x.Type)].  \mforall{}[f:Base].
    f  \mmember{}  per-function(A;x.B[x])  supposing  \mforall{}[a,a':Base].    (f  a)  =  (f  a')  supposing  a  =  a'


By

---

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

---

Home Index