---

Step * of Lemma member_sublist

∀[T:Type]. ∀L1,L2:T List.  (L1 ⊆ L2 ⇒ {∀x:T. ((x ∈ L1) ⇒ (x ∈ L2))})
BY
{ (Auto
   THEN AllHyps (Unfold `sublist`)
   THEN ExRepD
   THEN Unfold `l_member` 0
   THEN Auto
   THEN ExRepD
   THEN InstConcl [f i]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.    (L1  \msubseteq{}  L2  {}\mRightarrow{}  \{\mforall{}x:T.  ((x  \mmember{}  L1)  {}\mRightarrow{}  (x  \mmember{}  L2))\})


By

---

Latex:
(Auto
  THEN  AllHyps  (Unfold  `sublist`)
  THEN  ExRepD
  THEN  Unfold  `l\_member`  0
  THEN  Auto
  THEN  ExRepD
  THEN  InstConcl  [f  i]
  THEN  Auto)

---

Home Index