---

Step * of Lemma append-nil-sqle

∀[t:Top]. (t @ [] ≤ t)
BY
{ (Auto
   THEN RepUR ``append list_ind nil it cons`` 0
   THEN OneFixpointLeast
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((Reduce 0 THEN Strictness THEN Auto)))
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
   THEN Reduce 0
   THEN SqReasoning
   THEN Repeat (HVimplies2 0 [1])
   THEN ExceptionCases (-1)
   THEN Try (Trivial)
   THEN HVimplies2 (-2) [2]
   THEN (HVimplies2 (-3) [2] ORELSE (FLemma `exception-not-value` [-3] THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[t:Top].  (t  @  []  \mleq{}  t)


By

---

Latex:
(Auto
  THEN  RepUR  ``append  list\_ind  nil  it  cons``  0
  THEN  OneFixpointLeast
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((Reduce  0  THEN  Strictness  THEN  Auto)))
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  SqReasoning
  THEN  Repeat  (HVimplies2  0  [1])
  THEN  ExceptionCases  (-1)
  THEN  Try  (Trivial)
  THEN  HVimplies2  (-2)  [2]
  THEN  (HVimplies2  (-3)  [2]  ORELSE  (FLemma  `exception-not-value`  [-3]  THEN  Auto)))

---

Home Index