---

Step * of Lemma l_all-l_contains

∀[T:Type]. ∀[L1,L2:T List].  (L1 ⊆ L2 ⇒ (∀P:T ⟶ ℙ. ((∀x∈L2.P[x]) ⇒ (∀x∈L1.P[x]))))
BY
{ (Auto
   THEN ParallelLast
   THEN Auto
   THEN With ⌜i⌝ (D 4)⋅
   THEN Auto
   THEN D -1
   THEN RenameVar `j' (-2)
   THEN With ⌜j⌝ (D 5)⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  4)\mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  RenameVar  `j'  (-2)
  THEN  With  \mkleeneopen{}j\mkleeneclose{}  (D  5)\mcdot{}
  THEN  Auto)

---

Home Index