---

Step * 1 of Lemma length_functionality_wrt_permr


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

---

Latex:

---

Latex:

1.  A  :  Type
2.  as  :  A  List
3.  as'  :  A  List
4.  as  \mequiv{}(A)  as'
\mvdash{}  (For\{<\mBbbZ{}+>\}  x  \mmember{}  as.  1)  =  (For\{<\mBbbZ{}+>\}  x  \mmember{}  as'.  1)


By

---

Latex:
(RWH  (HypC  4)  0  THEN  Auto)

---

Home Index