---

Step * 1 of Lemma ppcc-test6


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 ∈ ℤ
BY
{ xxxxxxAuto'xxxxxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  as  :  A  List
5.  L  :  A  List
6.  n  :  \mBbbZ{}
7.  ||L||  =  ||as||
8.  ||L  @  as||  =  (n  +  n)
\mvdash{}  ||as||  =  n


By

---

Latex:
xxxxxxAuto'xxxxxx

---

Home Index