---

Step * 1 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-val(n + 1;bar-delay(x)) = (inl a) ∈ (T?)
BY
{ (Unfold `bar-delay` 0 THEN RecUnfold `bar-val` 0 THEN Reduce 0 THEN AutoSplit) }

---

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-val(n  +  1;bar-delay(x))  =  (inl  a)


By

---

Latex:
(Unfold  `bar-delay`  0  THEN  RecUnfold  `bar-val`  0  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index