---

Step * of Lemma provisional-type-cumulativity

No Annotations
∀[T:𝕌']. (Provisional(T) ⊆r Provisional'(T))
BY
{ (Auto THEN (D 0 THENA Auto) THEN D -1 THEN Unfold `provisional-type` 0) }

1
1. T : 𝕌'
2. x : Base
3. x1 : Base
4. x = x1 ∈ (x,y:ok:ℙ × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T))))
5. x ∈ ok:ℙ × T supposing ↓ok
6. x1 ∈ ok:ℙ × T supposing ↓ok
7. (↓fst(x) ⇐⇒ ↓fst(x1)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(x1)) ∈ T))
⊢ x = x1 ∈ (x,y:ok:ℙ' × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}'].  (Provisional(T)  \msubseteq{}r  Provisional'(T))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Unfold  `provisional-type`  0)

---

Home Index