---

Step * 1 2 1 of Lemma per-function-ext

.....subterm..... T:t
1:n
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;a.B a)]. ∀[a:A].  (f a ∈ B a)
7. a : Base
8. b : Base
9. c : a = b ∈ (per-function(A;x.B x) × per-function(A;x.B x))
⊢ (∀[a@0:A]. (((fst(a)) a@0) = ((snd(a)) a@0) ∈ (B a@0))) = (∀[a:A]. (((fst(b)) a) = ((snd(b)) a) ∈ (B a))) ∈ Type
BY
{ ((EqCD THEN Try (CompleteAuto))
   THEN (GenConcl ⌜a = v ∈ (per-function(A;x.B x) × per-function(A;x.B x))⌝⋅ THENA Auto)
   THEN (GenConcl ⌜b = u ∈ (per-function(A;x.B x) × per-function(A;x.B x))⌝⋅ THENA Auto)
   THEN DProdsAndUnions
   THEN Reduce 0) }

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;a.B a)]. ∀[a:A].  (f a ∈ B a)
7. a : Base
8. b : Base
9. c : a = b ∈ (per-function(A;x.B x) × per-function(A;x.B x))
10. a@0 : A
11. v1 : per-function(A;x.B x)
12. v2 : per-function(A;x.B x)
13. a = <v1, v2> ∈ (per-function(A;x.B x) × per-function(A;x.B x))
14. u1 : per-function(A;x.B x)
15. u2 : per-function(A;x.B x)
16. b = <u1, u2> ∈ (per-function(A;x.B x) × per-function(A;x.B x))
⊢ ((v1 a@0) = (v2 a@0) ∈ (B a@0)) = ((u1 a@0) = (u2 a@0) ∈ (B a@0)) ∈ ℙ

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  per-function(A;a.Type)  \mmember{}  \mBbbU{}'
3.  B  :  per-function(A;x.Type)
4.  \mforall{}[a:A].  (B  a  \mmember{}  Type)
5.  per-function(A;a.B  a)  \mmember{}  Type
6.  \mforall{}[f:per-function(A;a.B  a)].  \mforall{}[a:A].    (f  a  \mmember{}  B  a)
7.  a  :  Base
8.  b  :  Base
9.  c  :  a  =  b
\mvdash{}  (\mforall{}[a@0:A].  (((fst(a))  a@0)  =  ((snd(a))  a@0)))  =  (\mforall{}[a:A].  (((fst(b))  a)  =  ((snd(b))  a)))


By

---

Latex:
((EqCD  THEN  Try  (CompleteAuto))
  THEN  (GenConcl  \mkleeneopen{}a  =  v\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}b  =  u\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  Reduce  0)

---

Home Index