---

Step * 2 of Lemma in-bar-equal


1. [T] : Type
2. x : bar-base(T)
3. b : T
4. x↓b
⊢ bar-equal(T;x;in-bar(b))
BY
{ (D 0 THEN Auto) }

1
1. [T] : Type
2. x : bar-base(T)
3. b : T
4. x↓b
5. a : T
6. x↓a
⊢ in-bar(b)↓a

2
1. [T] : Type
2. x : bar-base(T)
3. b : T
4. x↓b
5. a : T
6. in-bar(b)↓a
⊢ x↓a

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  bar-base(T)
3.  b  :  T
4.  x\mdownarrow{}b
\mvdash{}  bar-equal(T;x;in-bar(b))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index