---

Step * 1 1 of Lemma bar-converges-unique


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?)
9. n ≤ n1
⊢ a = b ∈ T
BY
{ (InstLemma `bar-val-stable` [⌜T⌝;⌜n⌝;⌜x⌝;⌜n1⌝]⋅ THEN Auto) }

1
.....antecedent..... 
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?)
9. n ≤ n1
⊢ ↑isl(bar-val(n;x))

2
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?)
9. n ≤ n1
10. bar-val(n1;x) = bar-val(n;x) ∈ (T?)
⊢ a = b ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  bar-base(T)
3.  a  :  T
4.  b  :  T
5.  n1  :  \mBbbN{}@i
6.  bar-val(n1;x)  =  (inl  a)
7.  n  :  \mBbbN{}@i
8.  bar-val(n;x)  =  (inl  b)
9.  n  \mleq{}  n1
\mvdash{}  a  =  b


By

---

Latex:
(InstLemma  `bar-val-stable`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index