---

Step * 1 of Lemma per-product-elim


1. [A] : Type
2. [B] : per-function(A;a.Type)
3. [p] : per-product(A;a.B[a])
4. ∀[a:A]. (B[a] ∈ Type)
5. per-function(A;a.B[a]) ∈ Type
6. per-product(A;a.B[a]) ∈ Type
⊢ uand(p ~ <fst(p), snd(p)>;uand(fst(p) ∈ A;snd(p) ∈ B[fst(p)]))
BY
{ Assert ⌜p ~ <fst(p), snd(p)>⌝⋅ }

1
.....assertion..... 
1. [A] : Type
2. [B] : per-function(A;a.Type)
3. [p] : per-product(A;a.B[a])
4. ∀[a:A]. (B[a] ∈ Type)
5. per-function(A;a.B[a]) ∈ Type
6. per-product(A;a.B[a]) ∈ Type
⊢ p ~ <fst(p), snd(p)>

2
1. [A] : Type
2. [B] : per-function(A;a.Type)
3. [p] : per-product(A;a.B[a])
4. ∀[a:A]. (B[a] ∈ Type)
5. per-function(A;a.B[a]) ∈ Type
6. per-product(A;a.B[a]) ∈ Type
7. p ~ <fst(p), snd(p)>
⊢ uand(p ~ <fst(p), snd(p)>;uand(fst(p) ∈ A;snd(p) ∈ B[fst(p)]))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  per-function(A;a.Type)
3.  [p]  :  per-product(A;a.B[a])
4.  \mforall{}[a:A].  (B[a]  \mmember{}  Type)
5.  per-function(A;a.B[a])  \mmember{}  Type
6.  per-product(A;a.B[a])  \mmember{}  Type
\mvdash{}  uand(p  \msim{}  <fst(p),  snd(p)>uand(fst(p)  \mmember{}  A;snd(p)  \mmember{}  B[fst(p)]))


By

---

Latex:
Assert  \mkleeneopen{}p  \msim{}  <fst(p),  snd(p)>\mkleeneclose{}\mcdot{}

---

Home Index