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` THEN AbReduce 0) THEN THEN Auto) }

1
1. Type
2. as List
3. 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