---

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

No Annotations
∀[t:ListLike]. (t ≤ t @ [])
BY
{ (Auto
   THEN Refine_sqleDefinition `n'
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete (Refine_sqleZero))
   THEN Refine_divergentSqlen `y' ⌜Base⌝⋅
   THEN Try (Complete ((BLemma `is-list-if-has-value-hv-prp` THEN Auto)))) }

1
1. n : ℤ
2. 0 < n
3. ∀t:ListLike. (t ≤n - 1 t @ [])
4. t : ListLike
5. y : (t)↓
⊢ t ≤n t @ []

2
1. n : ℤ
2. 0 < n
3. ∀t:ListLike. (t ≤n - 1 t @ [])
4. t : ListLike
5. y : is-exception(t)
⊢ t ≤n t @ []

---

Latex:

---

Latex:
No  Annotations
\mforall{}[t:ListLike].  (t  \mleq{}  t  @  [])


By

---

Latex:
(Auto
  THEN  Refine\_sqleDefinition  `n'
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  (Refine\_sqleZero))
  THEN  Refine\_divergentSqlen  `y'  \mkleeneopen{}Base\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  ((BLemma  `is-list-if-has-value-hv-prp`  THEN  Auto))))

---

Home Index