---

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


1. K : Cname List
2. v : nameset(K) List
3. x : Cname
4. i : ℕ
5. i < ||v||
6. x = v[i] ∈ Cname
⊢ (x ∈ K)
BY
{ HypSubst' (-1) 0 }

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

---

Latex:

---

Latex:

1.  K  :  Cname  List
2.  v  :  nameset(K)  List
3.  x  :  Cname
4.  i  :  \mBbbN{}
5.  i  <  ||v||
6.  x  =  v[i]
\mvdash{}  (x  \mmember{}  K)


By

---

Latex:
HypSubst'  (-1)  0

---

Home Index