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