---

Step * 1 1 of Lemma co-value-height_wf


1. T : Type
2. co-value-height : T ⟶ partial(ℕ)
3. a1 : Base
4. (a1)↓
5. ↑is-atomic(a1)
6. x : a1 ~ <fst(a1), snd(a1)>
⊢ 1 + (co-value-height (fst(a1))) + (co-value-height (snd(a1))) ∈ partial(ℕ)
BY
{ (HypSubst' (-1) (-2) THEN RepUR ``is-atomic`` (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  co-value-height  :  T  {}\mrightarrow{}  partial(\mBbbN{})
3.  a1  :  Base
4.  (a1)\mdownarrow{}
5.  \muparrow{}is-atomic(a1)
6.  x  :  a1  \msim{}  <fst(a1),  snd(a1)>
\mvdash{}  1  +  (co-value-height  (fst(a1)))  +  (co-value-height  (snd(a1)))  \mmember{}  partial(\mBbbN{})


By

---

Latex:
(HypSubst'  (-1)  (-2)  THEN  RepUR  ``is-atomic``  (-2)  THEN  Auto)

---

Home Index