---

Step * 3 1 of Lemma per-or-equal


1. x : Base
2. A1 : Type
3. B1 : Type
4. A2 : Type
5. B2 : Type
6. B1 ≡ B2
7. A1 ≡ A2
8. y : Base
9. ispair(x) ~ tt
10. ispair(y) ~ tt
11. (fst(x)) = (fst(y)) ∈ per-value()
12. (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1 supposing (fst(x)) = (fst(x)) ∈ per-value()
13. fst(x) ∈ Base
14. (fst(x))↓
⊢ Ax ∈ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A2 otherwise B2 supposing (fst(x)) = (fst(x)) ∈ per-value()
BY
{ Auto }

1
1. x : Base
2. A1 : Type
3. B1 : Type
4. A2 : Type
5. B2 : Type
6. B1 ≡ B2
7. A1 ≡ A2
8. y : Base
9. ispair(x) ~ tt
10. ispair(y) ~ tt
11. (fst(x)) = (fst(y)) ∈ per-value()
12. fst(x) ∈ Base
13. (fst(x))↓
14. (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1
15. (fst(x)) = (fst(x)) ∈ per-value()
⊢ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A2 otherwise B2

---

Latex:

---

Latex:

1.  x  :  Base
2.  A1  :  Type
3.  B1  :  Type
4.  A2  :  Type
5.  B2  :  Type
6.  B1  \mequiv{}  B2
7.  A1  \mequiv{}  A2
8.  y  :  Base
9.  ispair(x)  \msim{}  tt
10.  ispair(y)  \msim{}  tt
11.  (fst(x))  =  (fst(y))
12.  (snd(x))  =  (snd(y))  supposing  (fst(x))  =  (fst(x))
13.  fst(x)  \mmember{}  Base
14.  (fst(x))\mdownarrow{}
\mvdash{}  Ax  \mmember{}  (snd(x))  =  (snd(y))  supposing  (fst(x))  =  (fst(x))


By

---

Latex:
Auto

---

Home Index