---

Step * 2 1 of Lemma bar-delay-equal

.....falsecase..... 
1. [T] : Type
2. x : bar-base(T)
3. a : T
4. n : ℕ
5. bar-val(n - 1;x) = (inl a) ∈ (T?)
6. ¬(n = 0 ∈ ℤ)
⊢ x↓a
BY
{ (With ⌜n - 1⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....falsecase..... 
1.  [T]  :  Type
2.  x  :  bar-base(T)
3.  a  :  T
4.  n  :  \mBbbN{}
5.  bar-val(n  -  1;x)  =  (inl  a)
6.  \mneg{}(n  =  0)
\mvdash{}  x\mdownarrow{}a


By

---

Latex:
(With  \mkleeneopen{}n  -  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index