---

Step * 1 1 2 2 2 1 1 of Lemma A-open-box-image_wf


1. K : Cname List
2. v : nameset(K) List
3. x : Cname
4. (x ∈ v)
⊢ (x ∈ K)
BY
{ RepeatFor 3 (D -1) }

1
1. K : Cname List
2. v : nameset(K) List
3. x : Cname
4. i : ℕ
5. i < ||v||
6. x = v[i] ∈ Cname
⊢ (x ∈ K)

---

Latex:

---

Latex:

1.  K  :  Cname  List
2.  v  :  nameset(K)  List
3.  x  :  Cname
4.  (x  \mmember{}  v)
\mvdash{}  (x  \mmember{}  K)


By

---

Latex:
RepeatFor  3  (D  -1)

---

Home Index