---

Step * of Lemma power-type-subtype-list

∀T:Type. ∀k:ℕ.  ((T^k) ⊆r (T List))
BY
{ (InductionOnNat THEN Reduce 0 THEN RecUnfold `power-type` 0 THEN Reduce 0 THEN Auto THEN AutoSplit THEN Auto') }

1
1. T : Type
2. k : ℤ
3. k ≠ 0
4. 0 < k
5. (T^k - 1) ⊆r (T List)
⊢ (T × (T^k - 1)) ⊆r (T List)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}k:\mBbbN{}.    ((T\^{}k)  \msubseteq{}r  (T  List))


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  RecUnfold  `power-type`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit
  THEN  Auto')

---

Home Index