---

Step * of Lemma sublist_map_inj

∀[A,B:Type].  ∀f:A ⟶ B. ∀as,bs:A List.  (Inj(A;B;f) ⇒ (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 Try (Complete ((RW ListC 0 THEN Auto)))
   THEN RW ListC (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}as,bs:A  List.    (Inj(A;B;f)  {}\mRightarrow{}  (as  \msubseteq{}  bs  \mLeftarrow{}{}\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  Try  (Complete  ((RW  ListC  0  THEN  Auto)))
  THEN  RW  ListC  (-1)
  THEN  Auto)

---

Home Index