---

Step * 1 2 of Lemma iota_wf


1. I : Cname List
2. x : Cname
⊢ ∀i,j:nameset(I).  ((↑isname(i)) ⇒ (↑isname(j)) ⇒ (i = j ∈ extd-nameset([x / I])) ⇒ (i = j ∈ nameset(I)))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

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

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  Cname
\mvdash{}  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(i))  {}\mRightarrow{}  (\muparrow{}isname(j))  {}\mRightarrow{}  (i  =  j)  {}\mRightarrow{}  (i  =  j))


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index