---

Step * 2 of Lemma rec-value-list-is-rec-value


1. u : rec-value()
2. v : rec-value() List
3. v ∈ rec-value()
⊢ [u / v] ∈ atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())
BY
{ ((BUnionRight THEN Auto) THEN (BUnionLeft THEN Auto) THEN Unfold `cons` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  rec-value()
2.  v  :  rec-value()  List
3.  v  \mmember{}  rec-value()
\mvdash{}  [u  /  v]  \mmember{}  atomic-values()  \mcup{}  (rec-value()  \mtimes{}  rec-value())  \mcup{}  (rec-value()  +  rec-value())


By

---

Latex:
((BUnionRight  THEN  Auto)  THEN  (BUnionLeft  THEN  Auto)  THEN  Unfold  `cons`  0  THEN  Auto)

---

Home Index