---

Step * 2 2 1 1 of Lemma rec-value-ext


1. a1 : Base@i
2. [%2] : (a1)↓@i
3. ↑is-atomic(a1)@i
4. x : a1 ~ <fst(a1), snd(a1)>
⊢ (1 + rec-value-height(fst(a1)) + rec-value-height(snd(a1)))↓
BY
{ (HypSubst' (-1) (-2) THEN RepUR ``is-atomic`` (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  Base@i
2.  [\%2]  :  (a1)\mdownarrow{}@i
3.  \muparrow{}is-atomic(a1)@i
4.  x  :  a1  \msim{}  <fst(a1),  snd(a1)>
\mvdash{}  (1  +  rec-value-height(fst(a1))  +  rec-value-height(snd(a1)))\mdownarrow{}


By

---

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

---

Home Index