---

Step * 1 of Lemma face-map_wf


1. L : Cname List
2. x : Cname
3. p : ℕ2
⊢ λz.if (z =z x) then p else z fi  ∈ nameset([x / L]) ⟶ extd-nameset(L)
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. z : nameset([x / L])
⊢ if (z =z x) then p else z fi  ∈ extd-nameset(L)

2
.....eq aux..... 
1. L : Cname List
2. x : Cname
3. p : ℕ2
⊢ nameset([x / L]) ∈ Type

---

Latex:

---

Latex:

1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
\mvdash{}  \mlambda{}z.if  (z  =\msubz{}  x)  then  p  else  z  fi    \mmember{}  nameset([x  /  L])  {}\mrightarrow{}  extd-nameset(L)


By

---

Latex:
MemCD

---

Home Index