---

Step * of Lemma l_all_subtype

∀[A,B:Type]. ∀[L:A List]. ∀[P:B ⟶ ℙ].  (∀x∈L.P[x]) ⇒ (∀x∈L.P[x]) supposing A ⊆r B
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].    (\mforall{}x\mmember{}L.P[x])  {}\mRightarrow{}  (\mforall{}x\mmember{}L.P[x])  supposing  A  \msubseteq{}r  B


By

---

Latex:
Auto

---

Home Index