---

Step * 2 of Lemma bar-delay-equal


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
BY
{ (Unfold `bar-delay` (-1) THEN RecUnfold `bar-val` (-1) THEN Reduce (-1) THEN SplitOnHypITE -1  THEN Auto)⋅ }

1
.....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

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `bar-delay`  (-1)
  THEN  RecUnfold  `bar-val`  (-1)
  THEN  Reduce  (-1)
  THEN  SplitOnHypITE  -1 
  THEN  Auto)\mcdot{}

---

Home Index