---

Step * of Lemma unshuffle_wf

∀[T:Type]. ∀[L:T List].  (unshuffle(L) ∈ (T × T) List)
BY
{ (InductionOnLength
   THEN RecUnfold `unshuffle` 0
   THEN Auto
   THEN Try ((BHyp (-2) THEN Auto))
   THEN ((DVar `L' THEN All Reduce THEN Auto) THEN DVar `v' THEN All Reduce THEN Auto' THEN D 0⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    (unshuffle(L)  \mmember{}  (T  \mtimes{}  T)  List)


By

---

Latex:
(InductionOnLength
  THEN  RecUnfold  `unshuffle`  0
  THEN  Auto
  THEN  Try  ((BHyp  (-2)  THEN  Auto))
  THEN  ((DVar  `L'  THEN  All  Reduce  THEN  Auto)
              THEN  DVar  `v'
              THEN  All  Reduce
              THEN  Auto'
              THEN  D  0\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index