---

Step * 2 1 1 1 1 1 of Lemma permutation-invariant2


1. T : Type
2. u : T
3. u1 : T
4. v : T List
⊢ ([u; [u1 / v]] o (0, 1)) = [u1; [u / v]] ∈ (T List)
BY
{ (BLemma `list_extensionality` THEN Auto') }

1
1. T : Type
2. u : T
3. u1 : T
4. v : T List
⊢ ||([u; [u1 / v]] o (0, 1))|| = ||[u1; [u / v]]|| ∈ ℤ

2
1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. i : ℕ@i
6. i < ||([u; [u1 / v]] o (0, 1))||
⊢ ([u; [u1 / v]] o (0, 1))[i] = [u1; [u / v]][i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  u1  :  T
4.  v  :  T  List
\mvdash{}  ([u;  [u1  /  v]]  o  (0,  1))  =  [u1;  [u  /  v]]


By

---

Latex:
(BLemma  `list\_extensionality`  THEN  Auto')

---

Home Index