---

Step * of Lemma per-function-ext

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

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

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  (InstLemma  `per-function\_wf\_type`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  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  RepeatFor  2  (Intro)
  THEN  (InstLemma  `apply-wf-per`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  (Unfold  `so\_apply`)
  THEN  Intro
  THEN  Try  ((UniverseIsType  THEN  Auto)))

---

Home Index