---

Step * 1 of Lemma is-list-prop1


1. t : Base
2. (is-list(t))↓
⊢ t ∈ Base List
BY
{ (RepUR ``is-list`` (-1)
   THEN Compactness (-1)
   THEN (Unhide THENA Auto)
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN RepeatFor 3 ((At ⌜Type⌝ (D 0)⋅ THENA Auto))
   THEN BotDiv
   THEN (RWO "fun_exp_unroll_1" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN HasValueD (-1)
   THEN HasValueImplies (-2) [1]
   THEN HypSubst (-1) (-3)
   THEN Reduce (-3)
   THEN HypSubst (-1) (-4)
   THEN RW UnrollLoopsOnceC' (-4)
   THEN Reduce (-4)
   THEN Try (Complete ((All (Fold `bottom`)
                        THEN InstHyp [⌜snd(t)⌝] 3⋅
                        THEN Auto
                        THEN Try ((HypSubst (-2) 0 THEN Fold `cons` 0 THEN Auto)))))
   THEN HasValueImplies (-3) [1]
   THEN HypSubst (-1) (-4)
   THEN AllReduce
   THEN BotDiv
   THEN HypSubst (-1) 0
   THEN Fold `it` 0
   THEN Fold `nil` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  t  :  Base
2.  (is-list(t))\mdownarrow{}
\mvdash{}  t  \mmember{}  Base  List


By

---

Latex:
(RepUR  ``is-list``  (-1)
  THEN  Compactness  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  RepeatFor  3  ((At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1)
  THEN  HasValueImplies  (-2)  [1]
  THEN  HypSubst  (-1)  (-3)
  THEN  Reduce  (-3)
  THEN  HypSubst  (-1)  (-4)
  THEN  RW  UnrollLoopsOnceC'  (-4)
  THEN  Reduce  (-4)
  THEN  Try  (Complete  ((All  (Fold  `bottom`)
                                            THEN  InstHyp  [\mkleeneopen{}snd(t)\mkleeneclose{}]  3\mcdot{}
                                            THEN  Auto
                                            THEN  Try  ((HypSubst  (-2)  0  THEN  Fold  `cons`  0  THEN  Auto)))))
  THEN  HasValueImplies  (-3)  [1]
  THEN  HypSubst  (-1)  (-4)
  THEN  AllReduce
  THEN  BotDiv
  THEN  HypSubst  (-1)  0
  THEN  Fold  `it`  0
  THEN  Fold  `nil`  0
  THEN  Auto)

---

Home Index