---

Step * of Lemma provisional-type-equality

No Annotations
∀[T:𝕌']. ∀[x,y:Provisional(T)].
  (x = y ∈ Provisional(T)) supposing ((allowed(x) ⇒ (allow(x) = allow(y) ∈ T)) and (allowed(x) ⇐⇒ allowed(y)))
BY
{ (Auto
   THEN D 3
   THEN D 2
   THEN Unfold `provisional-type` 0
   THEN QuotientEqTypeCDUp
   THEN Auto
   THEN All (Folds  ``allowed allow``)
   THEN Auto
   THEN ThinTrivial) }

1
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)
20. allow(x) = allow(x1) ∈ T
21. fst(x1)
⊢ ↓fst(y1)

2
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)

3
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}'].  \mforall{}[x,y:Provisional(T)].
    (x  =  y)  supposing  ((allowed(x)  {}\mRightarrow{}  (allow(x)  =  allow(y)))  and  (allowed(x)  \mLeftarrow{}{}\mRightarrow{}  allowed(y)))


By

---

Latex:
(Auto
  THEN  D  3
  THEN  D  2
  THEN  Unfold  `provisional-type`  0
  THEN  QuotientEqTypeCDUp
  THEN  Auto
  THEN  All  (Folds    ``allowed  allow``)
  THEN  Auto
  THEN  ThinTrivial)

---

Home Index