---

Step * of Lemma permr_weakening

∀T:Type. ∀as,bs:T List.  ((as = bs ∈ (T List)) ⇒ (as ≡(T) bs))
BY
{ Unfold `permr` 0   
THEN Auto }

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

---

Latex:

---

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


By

---

Latex:
Unfold  `permr`  0     
THEN  Auto

---

Home Index