---

Step * 1 of Lemma assert-exists_sublist


1. [T] : Type
⊢ ∀P:(T List) ⟶ 𝔹. (↑(P []) ⇐⇒ ∃LL:T List. (LL ⊆ [] ∧ (↑(P LL))))
BY
{ (Auto THEN ExRepD) }

1
1. T : Type
2. P : (T List) ⟶ 𝔹
3. LL : T List
4. LL ⊆ []
5. ↑(P LL)
⊢ ↑(P [])

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}P:(T  List)  {}\mrightarrow{}  \mBbbB{}.  (\muparrow{}(P  [])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}LL:T  List.  (LL  \msubseteq{}  []  \mwedge{}  (\muparrow{}(P  LL))))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index