---

Step * 4 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 A2 otherwise B2
13. fst(x) ∈ Base
14. (fst(x))↓
⊢ Ax ∈ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1 supposing (fst(x)) = (fst(x)) ∈ per-value()
BY
{ (MoveToConcl 12 THEN CanonicalTestCases⋅ THEN Auto) }

---

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))
13.  fst(x)  \mmember{}  Base
14.  (fst(x))\mdownarrow{}
\mvdash{}  Ax  \mmember{}  (snd(x))  =  (snd(y))  supposing  (fst(x))  =  (fst(x))


By

---

Latex:
(MoveToConcl  12  THEN  CanonicalTestCases\mcdot{}  THEN  Auto)

---

Home Index