---

Step * 1 1 2 of Lemma hd_two_swap_permr


1. T : Type
2. as : T List
3. a : T
4. a' : T
5. ((||as|| + 1) + 1) = ((||as|| + 1) + 1) ∈ ℤ
6. i : ℕ(||as|| + 1) + 1
7. i ≠ 1
8. i ≠ 0
⊢ [a; [a' / as]][i] = [a'; [a / as]][i] ∈ T
BY
{ (RewriteWith [] [`select_cons_tl`] 0 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  a  :  T
4.  a'  :  T
5.  ((||as||  +  1)  +  1)  =  ((||as||  +  1)  +  1)
6.  i  :  \mBbbN{}(||as||  +  1)  +  1
7.  i  \mneq{}  1
8.  i  \mneq{}  0
\mvdash{}  [a;  [a'  /  as]][i]  =  [a';  [a  /  as]][i]


By

---

Latex:
(RewriteWith  []  [`select\_cons\_tl`]  0  THEN  Auto')

---

Home Index