---

Step * 2 1 1 1 of Lemma face-map_wf


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])
12. ↑isname(i)
13. ↑isname(j)
⊢ (i = j ∈ extd-nameset(L)) ⇒ (i = j ∈ nameset([x / L]))
BY
{ ((Assert i ∈ nameset(L) BY
          OnMaybeHyp 6 (\h. (D h THEN MemTypeCD THEN Auto THEN (RW ListC (h+1) THENM D h+1) THEN Complete (Auto))))
   THEN (Assert j ∈ nameset(L) BY
               OnMaybeHyp 8 (\h. (D h THEN MemTypeCD THEN Auto THEN (RW ListC (h+1) THENM D h+1) THEN Complete (Auto))))
   ) }

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])
12. ↑isname(i)
13. ↑isname(j)
14. i ∈ nameset(L)
15. j ∈ nameset(L)
⊢ (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)
6.  i  :  nameset([x  /  L])
7.  i  \mneq{}  x
8.  j  :  nameset([x  /  L])
9.  j  \mneq{}  x
10.  i  \mmember{}  extd-nameset([x  /  L])
11.  j  \mmember{}  extd-nameset([x  /  L])
12.  \muparrow{}isname(i)
13.  \muparrow{}isname(j)
\mvdash{}  (i  =  j)  {}\mRightarrow{}  (i  =  j)


By

---

Latex:
((Assert  i  \mmember{}  nameset(L)  BY
                OnMaybeHyp  6  (\mbackslash{}h.  (D  h
                                                      THEN  MemTypeCD
                                                      THEN  Auto
                                                      THEN  (RW  ListC  (h+1)  THENM  D  h+1)
                                                      THEN  Complete  (Auto))))
  THEN  (Assert  j  \mmember{}  nameset(L)  BY
                          OnMaybeHyp  8  (\mbackslash{}h.  (D  h
                                                                THEN  MemTypeCD
                                                                THEN  Auto
                                                                THEN  (RW  ListC  (h+1)  THENM  D  h+1)
                                                                THEN  Complete  (Auto))))
  )

---

Home Index