---

Step * of Lemma l_all_sublist

∀[A:Type]. ∀P:A ⟶ ℙ. ∀as,bs:A List.  (as ⊆ bs ⇒ (∀x∈bs.P[x]) ⇒ (∀x∈as.P[x]))
BY
{ (Auto
   THEN (All(RWO "l_all_iff") THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (FLemma `member_sublist` [-4] THENA Auto)
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}as,bs:A  List.    (as  \msubseteq{}  bs  {}\mRightarrow{}  (\mforall{}x\mmember{}bs.P[x])  {}\mRightarrow{}  (\mforall{}x\mmember{}as.P[x]))


By

---

Latex:
(Auto
  THEN  (All(RWO  "l\_all\_iff")  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (FLemma  `member\_sublist`  [-4]  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index