---

Step * 1 2 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. y↓a1
⊢ x↓a1
BY
{ TACTIC:TACTIC:(FLemma `bar-converges-unique` [6; -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.  y\mdownarrow{}a1
\mvdash{}  x\mdownarrow{}a1


By

---

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

---

Home Index