---

Step * of Lemma length-insert-int

∀[T:Type]. ∀[x:T]. ∀[l:T List].  (||insert-int(x;l)|| = (||l|| + 1) ∈ ℤ) supposing T ⊆r ℤ
BY
{ (InductionOnList
   THEN Unfold `insert-int` 0
   THEN Reduce 0
   THEN Try (Fold `insert-int` 0⋅)
   THEN Auto
   THEN (CallByValueReduce 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[l:T  List].    (||insert-int(x;l)||  =  (||l||  +  1))  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(InductionOnList
  THEN  Unfold  `insert-int`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `insert-int`  0\mcdot{})
  THEN  Auto
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index