---

Step * 2 of Lemma equal-partial


1. T : Type
2. value-type(T)
3. x : partial(T)
4. y : partial(T)
5. uiff((x)↓;(y)↓) ∧ ((x)↓ ⇒ (x = y ∈ T))
⊢ x = y ∈ partial(T)
BY
{ (DVar  `x' THEN DVar `y' THEN EqTypeCD THEN Auto) }

1
1. T : Type
2. value-type(T)
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ base-partial(T)) ∧ (y ∈ base-partial(T)) ∧ per-partial(T;x;y)))
6. x ∈ base-partial(T)
7. x1 ∈ base-partial(T)
8. per-partial(T;x;x1)
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λx,y. ((x ∈ base-partial(T)) ∧ (y ∈ base-partial(T)) ∧ per-partial(T;x;y)))
12. y ∈ base-partial(T)
13. y1 ∈ base-partial(T)
14. per-partial(T;y;y1)
15. (y)↓ supposing (x)↓
16. (x)↓ supposing (y)↓
17. (x)↓ ⇒ (x = y ∈ T)
⊢ per-partial(T;x;y1)

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  x  :  partial(T)
4.  y  :  partial(T)
5.  uiff((x)\mdownarrow{};(y)\mdownarrow{})  \mwedge{}  ((x)\mdownarrow{}  {}\mRightarrow{}  (x  =  y))
\mvdash{}  x  =  y


By

---

Latex:
(DVar    `x'  THEN  DVar  `y'  THEN  EqTypeCD  THEN  Auto)

---

Home Index