---

Step * of Lemma interpolate-list_wf

∀[T:Type]. ∀[f:T ⟶ T ⟶ T]. ∀[L:T List].  (interpolate-list(x,y.f[x;y];L) ∈ T List) supposing value-type(T)
BY
{ (InductionOnList
   THEN Unfold `interpolate-list` 0
   THEN Reduce 0
   THEN ((MemCD THEN Trivial) ORELSE ((D -2 THEN Reduce 0) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[L:T  List].    (interpolate-list(x,y.f[x;y];L)  \mmember{}  T  List)  supposing  value-type(T)


By

---

Latex:
(InductionOnList
  THEN  Unfold  `interpolate-list`  0
  THEN  Reduce  0
  THEN  ((MemCD  THEN  Trivial)  ORELSE  ((D  -2  THEN  Reduce  0)  THEN  Auto)))

---

Home Index