---

Step * 1 of Lemma bag-member-sv-list


1. T : Type@i'
2. L : T List@i
3. single-valued-list(L;T)
4. x : T@i
5. \\%2 : ∃L@0:T List. ((L@0 = L ∈ bag(T)) ∧ (x ∈ L@0))@i
⊢ (x ∈ L)
BY
{ (With ⌈0⌉ (D 0)⋅
   THEN Auto
   THEN ExRepD
   THEN OnMaybeHyp 6 (\h. (EqTypeHD h
                           THEN Auto
                           THEN (FLemma `member-permutation` [h+3] THENA Auto)
                           THEN RWO "-1" (h+4)
                           THEN Auto))⋅) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  L  :  T  List@i
3.  single-valued-list(L;T)
4.  x  :  T@i
5.  \mbackslash{}\mbackslash{}\%2  :  \mexists{}L@0:T  List.  ((L@0  =  L)  \mwedge{}  (x  \mmember{}  L@0))@i
\mvdash{}  (x  \mmember{}  L)


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  ExRepD
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (EqTypeHD  h
                                                  THEN  Auto
                                                  THEN  (FLemma  `member-permutation`  [h+3]  THENA  Auto)
                                                  THEN  RWO  "-1"  (h+4)
                                                  THEN  Auto))\mcdot{})

---

Home Index