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