---

Step * of Lemma permr_inversion

∀T:Type. ∀as,bs:T List.  ((bs ≡(T) as) ⇒ (as ≡(T) bs))
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN ExRepD) }

1
1. T : Type
2. as : T List
3. bs : T List
4. ||bs|| = ||as|| ∈ ℤ
5. p : Sym(||bs||)
6. ∀i:ℕ||bs||. (bs[p.f i] = as[i] ∈ T)
⊢ ∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as,bs:T  List.    ((bs  \mequiv{}(T)  as)  {}\mRightarrow{}  (as  \mequiv{}(T)  bs))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  ExRepD)

---

Home Index