---

Step * of Lemma sqle-append-nil-if-has-value

∀[t:Base]. t ≤ t @ [] supposing (t)↓ ⇒ (is-list(t))↓
BY
{ ((Assert ∀t:Base. (is-exception(t) ⇒ (t ≤ t @ [])) BY
          (Intros THEN (ExceptionSqequal (-1) THEN RWO  "-1" 0) THEN Computation THEN Auto))
   THEN Auto
   THEN RepUR ``is-list`` (-1)
   THEN Compactness (-1)
   THEN (Unhide THENA Auto)
   THEN RepeatFor 2 (Thin (-3))
   THEN MoveToConcl 2
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Auto
   THEN BotDiv
   THEN (RWO "fun_exp_unroll_1" (-2) THENA Auto)
   THEN Reduce (-2)
   THEN (CallByValueReduce (-2) THENA Auto)
   THEN HasValueImplies (-2) [1]
   THEN Try (Complete ((HypSubst (-1) (-3)
                        THEN Thin (-1)
                        THEN HasValueImplies (-2) [1]
                        THEN Try (Complete ((HypSubst (-1) (-3) THEN BotDiv)))
                        THEN HypSubst (-1) 0
                        THEN Reduce 0
                        THEN Auto)))
   THEN HypSubst (-1) 0
   THEN Reduce 0
   THEN RepUR ``cons`` 0
   THEN SqLeCD
   THEN Try (Complete (Auto))
   THEN HypSubst (-1) (-3)
   THEN Reduce (-3)
   THEN BackThruSomeHyp
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  t  \mleq{}  t  @  []  supposing  (t)\mdownarrow{}  {}\mRightarrow{}  (is-list(t))\mdownarrow{}


By

---

Latex:
((Assert  \mforall{}t:Base.  (is-exception(t)  {}\mRightarrow{}  (t  \mleq{}  t  @  []))  BY
                (Intros  THEN  (ExceptionSqequal  (-1)  THEN  RWO    "-1"  0)  THEN  Computation  THEN  Auto))
  THEN  Auto
  THEN  RepUR  ``is-list``  (-1)
  THEN  Compactness  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-3))
  THEN  MoveToConcl  2
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  Auto
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll\_1"  (-2)  THENA  Auto)
  THEN  Reduce  (-2)
  THEN  (CallByValueReduce  (-2)  THENA  Auto)
  THEN  HasValueImplies  (-2)  [1]
  THEN  Try  (Complete  ((HypSubst  (-1)  (-3)
                                            THEN  Thin  (-1)
                                            THEN  HasValueImplies  (-2)  [1]
                                            THEN  Try  (Complete  ((HypSubst  (-1)  (-3)  THEN  BotDiv)))
                                            THEN  HypSubst  (-1)  0
                                            THEN  Reduce  0
                                            THEN  Auto)))
  THEN  HypSubst  (-1)  0
  THEN  Reduce  0
  THEN  RepUR  ``cons``  0
  THEN  SqLeCD
  THEN  Try  (Complete  (Auto))
  THEN  HypSubst  (-1)  (-3)
  THEN  Reduce  (-3)
  THEN  BackThruSomeHyp
  THEN  Trivial)

---

Home Index