---

Step * 1 2 of Lemma equipollent-list-as-product


1. [T] : Type
2. b : k:ℕ × (T^k)
⊢ ∃a:T List. (<||a||, a> = b ∈ (k:ℕ × (T^k)))
BY
{ (D -1
   THEN ((With ⌜b1⌝ (D 0)⋅ THEN Try ((EqualityIsType1 THEN Auto THEN BLemma `list-subtype-power-type` THEN Auto)))
         THENW Auto
         )
   ) }

1
1. T : Type
2. k : ℕ
3. b1 : (T^k)
⊢ <||b1||, b1> = <k, b1> ∈ (k:ℕ × (T^k))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  b  :  k:\mBbbN{}  \mtimes{}  (T\^{}k)
\mvdash{}  \mexists{}a:T  List.  (<||a||,  a>  =  b)


By

---

Latex:
(D  -1
  THEN  ((With  \mkleeneopen{}b1\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Try  ((EqualityIsType1  THEN  Auto  THEN  BLemma  `list-subtype-power-type`  THEN  Auto))
                )
              THENW  Auto
              )
  )

---

Home Index