---

Step * of Lemma equipollent-list

No Annotations
∀[T:Type]. ∀k:ℕ. (T ~ ℕk ⇒ (∀n:ℕ. {as:T List| ||as|| = n ∈ ℤ}  ~ ℕk^n))
BY
{ (Auto
   THEN ((InstLemma `equipollent-exp` [⌜n⌝;⌜k⌝]⋅ THENA Auto)
         THEN RWO "-1<" 0
         THEN Auto
         THEN RWO "3<" 0
         THEN Auto
         THEN ThinVar `k')⋅
   ) }

1
1. [T] : Type
2. n : ℕ
⊢ {as:T List| ||as|| = n ∈ ℤ}  ~ ℕn ⟶ T

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}k:\mBbbN{}.  (T  \msim{}  \mBbbN{}k  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \{as:T  List|  ||as||  =  n\}    \msim{}  \mBbbN{}k\^{}n))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `equipollent-exp`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  RWO  "-1<"  0
              THEN  Auto
              THEN  RWO  "3<"  0
              THEN  Auto
              THEN  ThinVar  `k')\mcdot{}
  )

---

Home Index