---

Step * 1 2 of Lemma partial-base


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

---

Latex:

---

Latex:

1.  x  :  base-partial(Base)
2.  x1  :  base-partial(Base)
3.  uiff((x)\mdownarrow{};(x1)\mdownarrow{})
4.  x  =  x1  supposing  (x)\mdownarrow{}
\mvdash{}  x1  =  x1


By

---

Latex:
TACTIC:Auto

---

Home Index