---

Step * of Lemma permutation_inversion

∀[A:Type]. ∀as,bs:A List.  (permutation(A;as;bs) ⇒ permutation(A;bs;as))
BY
{ ((Unfold `permutation` 0 THEN Auto)
   THEN ExRepD
   THEN (Assert ||as|| = ||bs|| ∈ ℤ BY
               ((HypSubst (-1) 0 THEN Auto) THEN RWO "permute_list_length" 0 THEN Auto))
   THEN (HypSubst (-2) 0 THENA Auto)
   THEN RWO "permute_permute_list" 0
   THEN Auto
   THEN Subst' ||(as o f)|| ~ ||as|| 0
   THEN Auto) }

1
1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
⊢ ∃f@0:ℕ||as|| ⟶ ℕ||as||. (Inj(ℕ||as||;ℕ||as||;f@0) ∧ (as = (as o f o f@0) ∈ (A List)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}as,bs:A  List.    (permutation(A;as;bs)  {}\mRightarrow{}  permutation(A;bs;as))


By

---

Latex:
((Unfold  `permutation`  0  THEN  Auto)
  THEN  ExRepD
  THEN  (Assert  ||as||  =  ||bs||  BY
                          ((HypSubst  (-1)  0  THEN  Auto)  THEN  RWO  "permute\_list\_length"  0  THEN  Auto))
  THEN  (HypSubst  (-2)  0  THENA  Auto)
  THEN  RWO  "permute\_permute\_list"  0
  THEN  Auto
  THEN  Subst'  ||(as  o  f)||  \msim{}  ||as||  0
  THEN  Auto)

---

Home Index