---

Step * of Lemma bar-delay-equal

∀[T:Type]. ∀x:bar-base(T). bar-equal(T;x;bar-delay(x))
BY
{ (Auto THEN D 0 THEN Auto THEN D -1) }

1
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

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:bar-base(T).  bar-equal(T;x;bar-delay(x))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  -1)

---

Home Index