---

Step * 2 1 of Lemma face-map_wf


1. L : Cname List
2. x : Cname
3. p : ℕ2
4. p ∈ extd-nameset([])
5. ¬↑isname(p)
⊢ ∀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])))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (Assert i ∈ extd-nameset([x / L]) BY
               Auto)
   THEN (Assert j ∈ extd-nameset([x / L]) BY
               Auto)
   THEN (BoolCase ⌜(i =z x)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜(j =z x)⌝⋅ THENA Auto)
   THEN Try (QuickAuto)) }

1
1. L : Cname List
2. x : Cname
3. p : ℕ2
4. p ∈ extd-nameset([])
5. ¬↑isname(p)
6. i : nameset([x / L])
7. i ≠ x
8. j : nameset([x / L])
9. j ≠ x
10. i ∈ extd-nameset([x / L])
11. j ∈ extd-nameset([x / L])
⊢ (↑isname(i)) ⇒ (↑isname(j)) ⇒ (i = j ∈ extd-nameset(L)) ⇒ (i = j ∈ nameset([x / L]))

---

Latex:

---

Latex:

1.  L  :  Cname  List
2.  x  :  Cname
3.  p  :  \mBbbN{}2
4.  p  \mmember{}  extd-nameset([])
5.  \mneg{}\muparrow{}isname(p)
\mvdash{}  \mforall{}i,j:nameset([x  /  L]).
        ((\muparrow{}isname(if  (i  =\msubz{}  x)  then  p  else  i  fi  ))
        {}\mRightarrow{}  (\muparrow{}isname(if  (j  =\msubz{}  x)  then  p  else  j  fi  ))
        {}\mRightarrow{}  (if  (i  =\msubz{}  x)  then  p  else  i  fi    =  if  (j  =\msubz{}  x)  then  p  else  j  fi  )
        {}\mRightarrow{}  (i  =  j))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (Assert  i  \mmember{}  extd-nameset([x  /  L])  BY
                          Auto)
  THEN  (Assert  j  \mmember{}  extd-nameset([x  /  L])  BY
                          Auto)
  THEN  (BoolCase  \mkleeneopen{}(i  =\msubz{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}(j  =\msubz{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (QuickAuto))

---

Home Index