---

Step * 1 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) ∈ ℤ
⊢ ∃p:Sym((||as|| + 1) + 1). ∀i:ℕ(||as|| + 1) + 1. ([a; [a' / as]][p.f i] = [a'; [a / as]][i] ∈ T)
BY
{ (With txpose_perm(0;1) (D 0) THEN Auto' THEN Reduce 0) }

1
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
⊢ [a; [a' / as]][swap(0;1) i] = [a'; [a / as]][i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  a  :  T
4.  a'  :  T
5.  ((||as||  +  1)  +  1)  =  ((||as||  +  1)  +  1)
\mvdash{}  \mexists{}p:Sym((||as||  +  1)  +  1).  \mforall{}i:\mBbbN{}(||as||  +  1)  +  1.  ([a;  [a'  /  as]][p.f  i]  =  [a';  [a  /  as]][i])


By

---

Latex:
(With  txpose\_perm(0;1)  (D  0)  THEN  Auto'  THEN  Reduce  0)

---

Home Index