---

Step * 1 of Lemma uext_wf


1. I : Cname List
2. J : Cname List
3. g : nameset(I) ⟶ extd-nameset(J)
4. z : extd-nameset(I)
5. ↑isname(z)
⊢ g z ∈ extd-nameset(J)
BY
{ (FLemma `assert-isname` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  g  :  nameset(I)  {}\mrightarrow{}  extd-nameset(J)
4.  z  :  extd-nameset(I)
5.  \muparrow{}isname(z)
\mvdash{}  g  z  \mmember{}  extd-nameset(J)


By

---

Latex:
(FLemma  `assert-isname`  [-1]  THEN  Auto)

---

Home Index