---

Step * of Lemma length_functionality_wrt_permr

∀A:Type. ∀as,as':A List.  ((as ≡(A) as') ⇒ (||as|| = ||as'|| ∈ ℤ))
BY
{ ((RepD THENM RWH (LemmaC `length_mon_for_char`) 0) THENA Auto) }

1
1. A : Type
2. as : A List
3. as' : A List
4. as ≡(A) as'
⊢ (For{<ℤ+>} x ∈ as. 1) = (For{<ℤ+>} x ∈ as'. 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}as,as':A  List.    ((as  \mequiv{}(A)  as')  {}\mRightarrow{}  (||as||  =  ||as'||))


By

---

Latex:
((RepD  THENM  RWH  (LemmaC  `length\_mon\_for\_char`)  0)  THENA  Auto)

---

Home Index