---

Step * 1 1 of Lemma assert-exists_sublist


1. T : Type
2. P : (T List) ⟶ 𝔹
3. LL : T List
4. LL ⊆ []
5. ↑(P LL)
⊢ ↑(P [])
BY
{ (FLemma `sublist_nil` [-2] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  LL  :  T  List
4.  LL  \msubseteq{}  []
5.  \muparrow{}(P  LL)
\mvdash{}  \muparrow{}(P  [])


By

---

Latex:
(FLemma  `sublist\_nil`  [-2]  THEN  Auto)

---

Home Index