---

Step * 2 1 of Lemma extend-name-morph_wf


1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
7. nameset(J) ⊆r extd-nameset([z2 / J])
8. i : nameset([z1 / I])
9. j : nameset([z1 / I])
10. ¬(j = z1 ∈ Cname)
11. i = z1 ∈ Cname
12. j ∈ nameset(I)
13. True
14. ↑isname(f j)
15. f j ∈ nameset(J)
16. z2 ∈ extd-nameset([z2 / J])
17. z2 = (f j) ∈ extd-nameset([z2 / J])
⊢ i = j ∈ nameset([z1 / I])
BY
{ (RevHypSubst' (-1) (-3) THEN MemTypeHD (-3) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  name-morph(I;J)
4.  z1  :  Cname
5.  z2  :  Cname
6.  \mneg{}(z2  \mmember{}  J)
7.  nameset(J)  \msubseteq{}r  extd-nameset([z2  /  J])
8.  i  :  nameset([z1  /  I])
9.  j  :  nameset([z1  /  I])
10.  \mneg{}(j  =  z1)
11.  i  =  z1
12.  j  \mmember{}  nameset(I)
13.  True
14.  \muparrow{}isname(f  j)
15.  f  j  \mmember{}  nameset(J)
16.  z2  \mmember{}  extd-nameset([z2  /  J])
17.  z2  =  (f  j)
\mvdash{}  i  =  j


By

---

Latex:
(RevHypSubst'  (-1)  (-3)  THEN  MemTypeHD  (-3)  THEN  Auto)

---

Home Index