---

Step * of Lemma face-map_wf

∀[L:Cname List]. ∀[x:Cname]. ∀[p:ℕ2].  ((x:=p) ∈ name-morph([x / L];L))
BY
{ (Auto THEN RepUR ``name-morph face-map`` 0 THEN MemTypeCD THEN Reduce 0) }

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

2
1. L : Cname List
2. x : Cname
3. p : ℕ2
⊢ ∀i,j:nameset([x / L]).
    ((↑isname(if (i =z x) then p else i fi ))
    ⇒ (↑isname(if (j =z x) then p else j fi ))
    ⇒ (if (i =z x) then p else i fi  = if (j =z x) then p else j fi  ∈ extd-nameset(L))
    ⇒ (i = j ∈ nameset([x / L])))

3
.....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

---

Latex:

---

Latex:
\mforall{}[L:Cname  List].  \mforall{}[x:Cname].  \mforall{}[p:\mBbbN{}2].    ((x:=p)  \mmember{}  name-morph([x  /  L];L))


By

---

Latex:
(Auto  THEN  RepUR  ``name-morph  face-map``  0  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index