---

Step * 1 of Lemma implies-bar-equal


1. [T] : Type
2. x : bar-base(T)@i
3. y : bar-base(T)@i
4. a : T@i
5. x↓a
6. y↓a
⊢ bar-equal(T;x;y)
BY
{ (D 0 THEN Auto) }

1
1. [T] : Type
2. x : bar-base(T)@i
3. y : bar-base(T)@i
4. a : T@i
5. x↓a
6. y↓a
7. a1 : T@i
8. x↓a1
⊢ y↓a1

2
1. [T] : Type
2. x : bar-base(T)@i
3. y : bar-base(T)@i
4. a : T@i
5. x↓a
6. y↓a
7. a1 : T@i
8. y↓a1
⊢ x↓a1

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  bar-base(T)@i
3.  y  :  bar-base(T)@i
4.  a  :  T@i
5.  x\mdownarrow{}a
6.  y\mdownarrow{}a
\mvdash{}  bar-equal(T;x;y)


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index