---

Step * 1 2 1 1 1 of Lemma iota_wf


1. I : Cname List
2. x : Cname
3. i : nameset(I)
4. j : nameset(I)
5. i ∈ extd-nameset(I)
6. j ∈ extd-nameset(I)
7. ↑isname(i)
8. ↑isname(j)
⊢ (i = j ∈ extd-nameset([x / I])) ⇒ (i = j ∈ nameset(I))
BY
{ ((Assert i ∈ nameset([x / I]) BY Auto) THEN (Assert j ∈ nameset([x / I]) BY Auto)) }

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

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  Cname
3.  i  :  nameset(I)
4.  j  :  nameset(I)
5.  i  \mmember{}  extd-nameset(I)
6.  j  \mmember{}  extd-nameset(I)
7.  \muparrow{}isname(i)
8.  \muparrow{}isname(j)
\mvdash{}  (i  =  j)  {}\mRightarrow{}  (i  =  j)


By

---

Latex:
((Assert  i  \mmember{}  nameset([x  /  I])  BY  Auto)  THEN  (Assert  j  \mmember{}  nameset([x  /  I])  BY  Auto))

---

Home Index