---

Step * of Lemma bar-converges-unique

∀[T:Type]. ∀[x:bar-base(T)]. ∀[a,b:T].  (x↓a ⇒ x↓b ⇒ (a = b ∈ T))
BY
{ TACTIC:(Unfold `bar-converges` 0 THEN Auto THEN ExRepD THEN Auto) }

1
1. T : Type
2. x : bar-base(T)
3. a : T
4. b : T
5. n1 : ℕ@i
6. bar-val(n1;x) = (inl a) ∈ (T?)
7. n : ℕ@i
8. bar-val(n;x) = (inl b) ∈ (T?)
⊢ a = b ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:bar-base(T)].  \mforall{}[a,b:T].    (x\mdownarrow{}a  {}\mRightarrow{}  x\mdownarrow{}b  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
TACTIC:(Unfold  `bar-converges`  0  THEN  Auto  THEN  ExRepD  THEN  Auto)

---

Home Index