---

Step * of Lemma sublist_map

∀[A,B:Type].  ∀f:A ⟶ B. ∀as,bs:A List.  (as ⊆ bs ⇒ map(f;as) ⊆ map(f;bs))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN All(RWO "length-map")
   THEN Auto
   THEN (InstHyp [⌜j⌝] (-3)⋅ THENA Auto)
   THEN RW ListC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}as,bs:A  List.    (as  \msubseteq{}  bs  {}\mRightarrow{}  map(f;as)  \msubseteq{}  map(f;bs))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  All(RWO  "length-map")
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  RW  ListC  0
  THEN  Auto)

---

Home Index