---

Step * of Lemma ppcc-test6

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as,L:A List]. ∀[n:ℤ].
  ||L @ as|| = (n + n) ∈ ℤ ⇐⇒ ||map(f;as)|| = n ∈ ℤ supposing ||L|| = ||as|| ∈ ℤ
BY
{ Auto⋅ }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. as : A List
5. L : A List
6. n : ℤ
7. ||L|| = ||as|| ∈ ℤ
8. ||L @ as|| = (n + n) ∈ ℤ
⊢ ||as|| = n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[as,L:A  List].  \mforall{}[n:\mBbbZ{}].
    ||L  @  as||  =  (n  +  n)  \mLeftarrow{}{}\mRightarrow{}  ||map(f;as)||  =  n  supposing  ||L||  =  ||as||


By

---

Latex:
Auto\mcdot{}

---

Home Index