---

Step * of Lemma bar-val-diverge

∀[T:Type]. ∀[n:ℕ].  (bar-val(n;diverge()) ~ inr ⋅ )
BY
{ (InductionOnNat THEN RecUnfold `bar-val` 0 THEN RecUnfold `diverge` 0 THEN Reduce 0 THEN Auto THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].    (bar-val(n;diverge())  \msim{}  inr  \mcdot{}  )


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `bar-val`  0
  THEN  RecUnfold  `diverge`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index