---

Step * 1 1 1 of Lemma face-map_wf


1. L : Cname List
2. x : Cname
3. p : ℕ2
4. z : Cname
5. (z ∈ [x / L])
6. z = x ∈ ℤ
⊢ p ∈ extd-nameset(L)
BY
{ Auto }

---

Latex:

---

Latex:

1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  z  :  Cname
5.  (z  \mmember{}  [x  /  L])
6.  z  =  x
\mvdash{}  p  \mmember{}  extd-nameset(L)


By

---

Latex:
Auto

---

Home Index