---

Step * of Lemma equipollent-list-as-product

∀[T:Type]. T List ~ k:ℕ × (T^k)
BY
{ (Auto THEN With ⌜λL.<||L||, L>⌝ (D 0)⋅ THEN Auto THEN Try ((BLemma `list-subtype-power-type` THEN Auto))) }

1
1. [T] : Type
⊢ Bij(T List;k:ℕ × (T^k);λL.<||L||, L>)

---

Latex:

---

Latex:
\mforall{}[T:Type].  T  List  \msim{}  k:\mBbbN{}  \mtimes{}  (T\^{}k)


By

---

Latex:
(Auto
  THEN  With  \mkleeneopen{}\mlambda{}L.<||L||,  L>\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `list-subtype-power-type`  THEN  Auto)))

---

Home Index