---

Step * 2 1 1 1 1 of Lemma assert-exists-l_subset


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. LL : T List
4. l_subset(T;LL;[])
⊢ ∃LLL:T List. (LLL ⊆ [] ∧ set-equal(T;LLL;LL))
BY
{ (FLemma `l_subset_nil_right` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  LL  :  T  List
4.  l\_subset(T;LL;[])
\mvdash{}  \mexists{}LLL:T  List.  (LLL  \msubseteq{}  []  \mwedge{}  set-equal(T;LLL;LL))


By

---

Latex:
(FLemma  `l\_subset\_nil\_right`  [-1]  THEN  Auto)

---

Home Index