---

Step * of Lemma tuple-type-monotone

∀[P:Type]. ∀[F,G:P ⟶ Type].  ∀[v:P List]. (tuple-type(map(F;v)) ⊆r tuple-type(map(G;v))) supposing F ⊆ G
BY
{ (InductionOnList THEN Reduce 0 THEN (((RWO "null-map" 0 THENA Auto) THEN AutoSplit) ORELSE Auto)) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[F,G:P  {}\mrightarrow{}  Type].
    \mforall{}[v:P  List].  (tuple-type(map(F;v))  \msubseteq{}r  tuple-type(map(G;v)))  supposing  F  \msubseteq{}  G


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  (((RWO  "null-map"  0  THENA  Auto)  THEN  AutoSplit)  ORELSE  Auto))

---

Home Index