---

Step * of Lemma uext_wf

∀[I,J:Cname List]. ∀[g:nameset(I) ⟶ extd-nameset(J)].  (uext(g) ∈ extd-nameset(I) ⟶ extd-nameset(J))
BY
{ (Auto THEN Unfold `uext` 0 THEN (MemCD THENA Auto) THEN (BoolCase ⌜isname(z)⌝⋅ THENA Auto)) }

1
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)

2
1. I : Cname List
2. J : Cname List
3. g : nameset(I) ⟶ extd-nameset(J)
4. z : extd-nameset(I)
5. ¬↑isname(z)
⊢ z ∈ extd-nameset(J)

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[g:nameset(I)  {}\mrightarrow{}  extd-nameset(J)].
    (uext(g)  \mmember{}  extd-nameset(I)  {}\mrightarrow{}  extd-nameset(J))


By

---

Latex:
(Auto  THEN  Unfold  `uext`  0  THEN  (MemCD  THENA  Auto)  THEN  (BoolCase  \mkleeneopen{}isname(z)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index