---

Step * 2 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. (↓fst(x)) ⇐ ↓fst(x1)
9. (↓fst(x)) ⇒ (allow(x) = allow(x1) ∈ T)
10. y : Base
11. y1 : Base
12. y = y1 ∈ (x,y:ok:ℙ × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ (allow(x) = allow(y) ∈ T))))
13. y ∈ ok:ℙ × T supposing ↓ok
14. y1 ∈ ok:ℙ × T supposing ↓ok
15. (↓fst(y)) ⇒ (↓fst(y1))
16. (↓fst(y)) ⇐ ↓fst(y1)
17. (↓fst(y)) ⇒ (allow(y) = allow(y1) ∈ T)
18. allowed(x) ⇒ allowed(y)
19. allowed(x) ⇐ allowed(y)
20. allowed(x) ⇒ (allow(x) = allow(y) ∈ T)
21. fst(y1)
⊢ ↓fst(x)
BY
{ ((Assert ↓fst(y1) BY
          Auto)
   THEN (Assert ↓fst(y) BY
               Auto)
   THEN (Assert allowed(y1) BY
               (Unfold `allowed` 0 THEN EAuto 1))
   THEN (Assert allowed(y) BY
               (Unfold `allowed` 0 THEN EAuto 1))
   THEN ThinTrivial
   THEN All (Unfold `allowed`)
   THEN EAuto 1) }

---

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))  {}\mRightarrow{}  (\mdownarrow{}fst(x1))
8.  (\mdownarrow{}fst(x))  \mLeftarrow{}{}  \mdownarrow{}fst(x1)
9.  (\mdownarrow{}fst(x))  {}\mRightarrow{}  (allow(x)  =  allow(x1))
10.  y  :  Base
11.  y1  :  Base
12.  y  =  y1
13.  y  \mmember{}  ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok
14.  y1  \mmember{}  ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok
15.  (\mdownarrow{}fst(y))  {}\mRightarrow{}  (\mdownarrow{}fst(y1))
16.  (\mdownarrow{}fst(y))  \mLeftarrow{}{}  \mdownarrow{}fst(y1)
17.  (\mdownarrow{}fst(y))  {}\mRightarrow{}  (allow(y)  =  allow(y1))
18.  allowed(x)  {}\mRightarrow{}  allowed(y)
19.  allowed(x)  \mLeftarrow{}{}  allowed(y)
20.  allowed(x)  {}\mRightarrow{}  (allow(x)  =  allow(y))
21.  fst(y1)
\mvdash{}  \mdownarrow{}fst(x)


By

---

Latex:
((Assert  \mdownarrow{}fst(y1)  BY
                Auto)
  THEN  (Assert  \mdownarrow{}fst(y)  BY
                          Auto)
  THEN  (Assert  allowed(y1)  BY
                          (Unfold  `allowed`  0  THEN  EAuto  1))
  THEN  (Assert  allowed(y)  BY
                          (Unfold  `allowed`  0  THEN  EAuto  1))
  THEN  ThinTrivial
  THEN  All  (Unfold  `allowed`)
  THEN  EAuto  1)

---

Home Index