---

Step * of Lemma has-value-is-list-approx-is-type

∀[T:Type]. ∀[t:colist(T)]. ∀[n:ℕ].
  ((λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥^n ⊥ t)↓ ∈ Typ\000Ce)
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN ((((D 0 THENA Auto) THEN (RWO "fun_exp_unroll" 0 THENA Auto))
          THEN (BoolCase ⌜(n =z 0)⌝⋅ THENA Auto)
          THEN ((CallByValueReduce 0 THENA Auto) ORELSE Auto)
          THEN CoListD (-1)
          THEN Reduce 0
          THEN Auto)
   ORELSE (Strictness THEN Auto)
   )) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].  \mforall{}[n:\mBbbN{}].
    ((\mlambda{}is-list,t.  eval  u  =  t  in
                                if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}\^{}n 
        \mbot{} 
        t)\mdownarrow{}  \mmember{}  Type)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  ((((D  0  THENA  Auto)  THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto))
                THEN  (BoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  ((CallByValueReduce  0  THENA  Auto)  ORELSE  Auto)
                THEN  CoListD  (-1)
                THEN  Reduce  0
                THEN  Auto)
  ORELSE  (Strictness  THEN  Auto)
  ))

---

Home Index