---

Step * of Lemma assert-exists-l_subset

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀P:(T List) ⟶ 𝔹
        ((∀L1,L2:T List.  (set-equal(T;L1;L2) ⇒ (↑(P L1) ⇐⇒ ↑(P L2))))
        ⇒ (∀L:T List. (↑exists_sublist(L;P) ⇐⇒ ∃LL:T List. (l_subset(T;LL;L) ∧ (↑(P LL))))))))
BY
{ (RepeatFor 4 (Intro) THEN RWO "assert-exists_sublist" 0 THEN Auto) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. P : (T List) ⟶ 𝔹
4. ∀L1,L2:T List.  (set-equal(T;L1;L2) ⇒ (↑(P L1) ⇐⇒ ↑(P L2)))
5. L : T List
6. ∃LL:T List. (LL ⊆ L ∧ (↑(P LL)))
⊢ ∃LL:T List. (l_subset(T;LL;L) ∧ (↑(P LL)))

2
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. P : (T List) ⟶ 𝔹
4. ∀L1,L2:T List.  (set-equal(T;L1;L2) ⇒ (↑(P L1) ⇐⇒ ↑(P L2)))
5. L : T List
6. ∃LL:T List. (l_subset(T;LL;L) ∧ (↑(P LL)))
⊢ ∃LL:T List. (LL ⊆ L ∧ (↑(P LL)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}P:(T  List)  {}\mrightarrow{}  \mBbbB{}
                ((\mforall{}L1,L2:T  List.    (set-equal(T;L1;L2)  {}\mRightarrow{}  (\muparrow{}(P  L1)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(P  L2))))
                {}\mRightarrow{}  (\mforall{}L:T  List.  (\muparrow{}exists\_sublist(L;P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}LL:T  List.  (l\_subset(T;LL;L)  \mwedge{}  (\muparrow{}(P  LL))))))))


By

---

Latex:
(RepeatFor  4  (Intro)  THEN  RWO  "assert-exists\_sublist"  0  THEN  Auto)

---

Home Index