---

Step * of Lemma list-subtype-power-type

∀T:Type. ∀L:T List.  (L ∈ (T^||L||))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN RecUnfold `power-type` 0
   THEN Reduce 0
   THEN Try ((Unfold `nil` 0 THEN Auto))
   THEN AutoSplit
   THEN Auto') }

1
1. T : Type
2. u : T
3. v : T List
4. ||v|| + 1 ≠ 0
5. v ∈ (T^||v||)
⊢ [u / v] ∈ T × (T^(||v|| + 1) - 1)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L:T  List.    (L  \mmember{}  (T\^{}||L||))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  RecUnfold  `power-type`  0
  THEN  Reduce  0
  THEN  Try  ((Unfold  `nil`  0  THEN  Auto))
  THEN  AutoSplit
  THEN  Auto')

---

Home Index