---

Step * 1 of Lemma bar-delay-equal


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

1
1. T : Type
2. x : bar-base(T)
3. a : T
4. n : ℕ
5. bar-val(n;x) = (inl a) ∈ (T?)
⊢ bar-val(n + 1;bar-delay(x)) = (inl a) ∈ (T?)

---

Latex:

---

Latex:

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


By

---

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

---

Home Index