---

Step * 3 of Lemma face-map_wf

.....wf..... 
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. f : nameset([x / L]) ⟶ extd-nameset(L)
⊢ ∀i,j:nameset([x / L]).
    ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(L)) ⇒ (i = j ∈ nameset([x / L]))) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  f  :  nameset([x  /  L])  {}\mrightarrow{}  extd-nameset(L)
\mvdash{}  \mforall{}i,j:nameset([x  /  L]).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index