---

Step * 1 of Lemma partial-base


1. x : base-partial(Base)
2. x1 : base-partial(Base)
3. per-partial(Base;x;x1)
⊢ x = x1 ∈ Base
BY
{ TACTIC:(D (-1) THEN Subst' x ~ x1 0)⋅ }

1
.....equality..... 
1. x : base-partial(Base)
2. x1 : base-partial(Base)
3. uiff((x)↓;(x1)↓)
4. x = x1 ∈ Base supposing (x)↓
⊢ x ~ x1

2
1. x : base-partial(Base)
2. x1 : base-partial(Base)
3. uiff((x)↓;(x1)↓)
4. x = x1 ∈ Base supposing (x)↓
⊢ x1 = x1 ∈ Base

---

Latex:

---

Latex:

1.  x  :  base-partial(Base)
2.  x1  :  base-partial(Base)
3.  per-partial(Base;x;x1)
\mvdash{}  x  =  x1


By

---

Latex:
TACTIC:(D  (-1)  THEN  Subst'  x  \msim{}  x1  0)\mcdot{}

---

Home Index