---

Step * 2 1 of Lemma equal-partial


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)
BY
{ (InstLemma `per-partial-equiv_rel` [⌜T⌝]⋅ THENA 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)
18. EquivRel(base-partial(T);x,y.per-partial(T;x;y))
⊢ per-partial(T;x;y1)

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  x  :  Base
4.  x1  :  Base
5.  x  =  x1
6.  x  \mmember{}  base-partial(T)
7.  x1  \mmember{}  base-partial(T)
8.  per-partial(T;x;x1)
9.  y  :  Base
10.  y1  :  Base
11.  y  =  y1
12.  y  \mmember{}  base-partial(T)
13.  y1  \mmember{}  base-partial(T)
14.  per-partial(T;y;y1)
15.  (y)\mdownarrow{}  supposing  (x)\mdownarrow{}
16.  (x)\mdownarrow{}  supposing  (y)\mdownarrow{}
17.  (x)\mdownarrow{}  {}\mRightarrow{}  (x  =  y)
\mvdash{}  per-partial(T;x;y1)


By

---

Latex:
(InstLemma  `per-partial-equiv\_rel`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index