---

Step * 3 of Lemma provisional-type-equality


1. T : 𝕌'
2. x : Base
3. x1 : Base
4. x = x1 ∈ (x,y:ok:ℙ × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ (allow(x) = allow(y) ∈ T))))
5. x ∈ ok:ℙ × T supposing ↓ok
6. x1 ∈ ok:ℙ × T supposing ↓ok
7. (↓fst(x)) ⇐ ↓fst(x1)
8. y : Base
9. y1 : Base
10. y = y1 ∈ (x,y:ok:ℙ × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ (allow(x) = allow(y) ∈ T))))
11. y ∈ ok:ℙ × T supposing ↓ok
12. y1 ∈ ok:ℙ × T supposing ↓ok
13. (↓fst(y)) ⇒ (↓fst(y1))
14. (↓fst(y)) ⇐ ↓fst(y1)
15. (↓fst(y)) ⇒ (allow(y) = allow(y1) ∈ T)
16. allowed(x) ⇒ allowed(y)
17. allowed(x) ⇐ allowed(y)
18. allowed(x) ⇒ (allow(x) = allow(y) ∈ T)
19. (↓fst(x)) ⇐ ↓fst(y1)
20. fst(x)
21. fst(y1)
22. allow(x) = allow(x1) ∈ T
23. fst(x1)
⊢ allow(x) = allow(y1) ∈ T
BY
{ ((Assert allowed(x) BY
          (Unfold `allowed` 0 THEN BLemma `squash-implies-usquash` THEN Auto))
   THEN (Assert allowed(x1) BY
               (Unfold `allowed` 0 THEN BLemma `squash-implies-usquash` THEN Auto))
   THEN (Assert ↓fst(x) BY
               Auto)
   THEN (Assert ↓fst(x1) BY
               Auto)
   THEN ThinTrivial
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  \mBbbU{}'
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok
6.  x1  \mmember{}  ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok
7.  (\mdownarrow{}fst(x))  \mLeftarrow{}{}  \mdownarrow{}fst(x1)
8.  y  :  Base
9.  y1  :  Base
10.  y  =  y1
11.  y  \mmember{}  ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok
12.  y1  \mmember{}  ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok
13.  (\mdownarrow{}fst(y))  {}\mRightarrow{}  (\mdownarrow{}fst(y1))
14.  (\mdownarrow{}fst(y))  \mLeftarrow{}{}  \mdownarrow{}fst(y1)
15.  (\mdownarrow{}fst(y))  {}\mRightarrow{}  (allow(y)  =  allow(y1))
16.  allowed(x)  {}\mRightarrow{}  allowed(y)
17.  allowed(x)  \mLeftarrow{}{}  allowed(y)
18.  allowed(x)  {}\mRightarrow{}  (allow(x)  =  allow(y))
19.  (\mdownarrow{}fst(x))  \mLeftarrow{}{}  \mdownarrow{}fst(y1)
20.  fst(x)
21.  fst(y1)
22.  allow(x)  =  allow(x1)
23.  fst(x1)
\mvdash{}  allow(x)  =  allow(y1)


By

---

Latex:
((Assert  allowed(x)  BY
                (Unfold  `allowed`  0  THEN  BLemma  `squash-implies-usquash`  THEN  Auto))
  THEN  (Assert  allowed(x1)  BY
                          (Unfold  `allowed`  0  THEN  BLemma  `squash-implies-usquash`  THEN  Auto))
  THEN  (Assert  \mdownarrow{}fst(x)  BY
                          Auto)
  THEN  (Assert  \mdownarrow{}fst(x1)  BY
                          Auto)
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index