---

Step * of Lemma equal-partial

∀[T:Type]. ∀[x,y:partial(T)].  uiff(x = y ∈ partial(T);uiff((x)↓;(y)↓) ∧ ((x)↓ ⇒ (x = y ∈ T))) supposing value-type(T)
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. T : Type
2. value-type(T)
3. x : partial(T)
4. y : partial(T)
5. x = y ∈ partial(T)
⊢ uiff((x)↓;(y)↓) ∧ ((x)↓ ⇒ (x = y ∈ T))

2
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)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[x,y:partial(T)].    uiff(x  =  y;uiff((x)\mdownarrow{};(y)\mdownarrow{})  \mwedge{}  ((x)\mdownarrow{}  {}\mRightarrow{}  (x  =  y)))  supposing  value-type(T)


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index