---

Step * 1 2 of Lemma respects-equality-list-type


1. A : Type
2. B : Type
3. respects-equality(A;B)
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (v[i] ∈ B)) ⇒ (v ∈ B List)
⊢ (∀i:ℕ||[u / v]||. ([u / v][i] ∈ B)) ⇒ ([u / v] ∈ B List)
BY
{ ((D 0 THENA Auto) THEN MemCD) }

1
.....implicit subterm..... 
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (v[i] ∈ B)) ⇒ (v ∈ B List)
7. ∀i:ℕ||[u / v]||. ([u / v][i] ∈ B)
⊢ B ∈ Type

2
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (v[i] ∈ B)) ⇒ (v ∈ B List)
7. ∀i:ℕ||[u / v]||. ([u / v][i] ∈ B)
⊢ u ∈ B

3
.....subterm..... T:t
2:n
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (v[i] ∈ B)) ⇒ (v ∈ B List)
7. ∀i:ℕ||[u / v]||. ([u / v][i] ∈ B)
⊢ v ∈ B List

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  respects-equality(A;B)
4.  u  :  A
5.  v  :  A  List
6.  (\mforall{}i:\mBbbN{}||v||.  (v[i]  \mmember{}  B))  {}\mRightarrow{}  (v  \mmember{}  B  List)
\mvdash{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  ([u  /  v][i]  \mmember{}  B))  {}\mRightarrow{}  ([u  /  v]  \mmember{}  B  List)


By

---

Latex:
((D  0  THENA  Auto)  THEN  MemCD)

---

Home Index