---

Step * of Lemma sublist_tl2

∀[T:Type]. ∀u:T. ∀v,L1:T List.  (L1 ⊆ v ⇒ L1 ⊆ [u / v])
BY
{ Auto }

1
1. [T] : Type
2. u : T
3. v : T List
4. L1 : T List
5. L1 ⊆ v
⊢ L1 ⊆ [u / v]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}u:T.  \mforall{}v,L1:T  List.    (L1  \msubseteq{}  v  {}\mRightarrow{}  L1  \msubseteq{}  [u  /  v])


By

---

Latex:
Auto

---

Home Index