---

Step * 1 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
7. a1 : T@i
8. x↓a1
⊢ y↓a1
BY
{ TACTIC:(FLemma `bar-converges-unique` [5; -1] THEN Auto) }

---

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
7.  a1  :  T@i
8.  x\mdownarrow{}a1
\mvdash{}  y\mdownarrow{}a1


By

---

Latex:
TACTIC:(FLemma  `bar-converges-unique`  [5;  -1]  THEN  Auto)

---

Home Index