---

Step * of Lemma pairwise-sublist

∀[T:Type]. ∀L1,L2:T List.  ∀[P:T ⟶ T ⟶ ℙ']. (L1 ⊆ L2 ⇒ (∀x,y∈L2.  P[x;y]) ⇒ (∀x,y∈L1.  P[x;y]))
BY
{ Auto }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. [P] : T ⟶ T ⟶ ℙ'
5. L1 ⊆ L2
6. (∀x,y∈L2.  P[x;y])
⊢ (∀x,y∈L1.  P[x;y])

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index