---

Step * of Lemma hd_two_swap_permr

∀T:Type. ∀as:T List. ∀a,a':T.  ([a; [a' / as]] ≡(T) [a'; [a / as]])
BY
{ (Auto THEN (Unfold `permr` 0 THEN AbReduce 0) THEN D 0 THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as:T  List.  \mforall{}a,a':T.    ([a;  [a'  /  as]]  \mequiv{}(T)  [a';  [a  /  as]])


By

---

Latex:
(Auto  THEN  (Unfold  `permr`  0  THEN  AbReduce  0)  THEN  D  0  THEN  Auto)

---

Home Index