---

Step * of Lemma iseg-map

∀[A,B:Type].  ∀f:A ⟶ B. ∀L1,L2:A List.  (L1 ≤ L2 ⇒ map(f;L1) ≤ map(f;L2))
BY
{ (Auto THEN D -1 THEN HypSubst' -1 0 THEN (RWO "map_append_sq" 0 THENA Auto) THEN With ⌜map(f;l)⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}L1,L2:A  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  map(f;L1)  \mleq{}  map(f;L2))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  HypSubst'  -1  0
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
  THEN  With  \mkleeneopen{}map(f;l)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index