---

Step * 2 of Lemma per-or-equal


1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. B1 ≡ B2
6. A1 ≡ A2
7. x : Base
8. y : Base
⊢ uand(ispair(x) ~ tt;uand(ispair(y) ~ tt;uand((fst(x)) = (fst(y)) ∈ per-value();(snd(x))
                                                                                 = (snd(y))
                                                                                 ∈ if fst(x) = Ax then A2 otherwise B2 
                                                                                 supposing (fst(x))
                                                                                 = (fst(y))
                                                                                 ∈ per-value()))) ∈ Type
BY
{ RepeatFor 4 ((MemCD THEN Try (QuickAuto))⋅)⋅ }

1
.....subterm..... T:t
2:n
1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. B1 ≡ B2
6. A1 ≡ A2
7. x : Base
8. y : Base
9. (fst(x)) = (fst(y)) ∈ per-value()
⊢ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A2 otherwise B2 ∈ Type

---

Latex:

---

Latex:

1.  A1  :  Type
2.  B1  :  Type
3.  A2  :  Type
4.  B2  :  Type
5.  B1  \mequiv{}  B2
6.  A1  \mequiv{}  A2
7.  x  :  Base
8.  y  :  Base
\mvdash{}  uand(ispair(x)  \msim{}  tt;uand(ispair(y)  \msim{}  tt;uand((fst(x))  =  (fst(y));(snd(x))  =  (snd(y)) 
                                                                                                                                      supposing  (fst(x))  =  (fst(y)))))
    \mmember{}  Type


By

---

Latex:
RepeatFor  4  ((MemCD  THEN  Try  (QuickAuto))\mcdot{})\mcdot{}

---

Home Index