---

Step * 1 1 2 1 of Lemma face-map_wf

.....set predicate..... 
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. z : Cname
5. z ≠ x
6. (z ∈ [x / L])
⊢ (z ∈ L)
BY
{ ((RW ListC (-1) THEN Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  z  :  Cname
5.  z  \mneq{}  x
6.  (z  \mmember{}  [x  /  L])
\mvdash{}  (z  \mmember{}  L)


By

---

Latex:
((RW  ListC  (-1)  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index