---

Step * 1 of Lemma l_contains-cons


1. [T] : Type
2. u : T
3. v : T List
4. bs : T List
5. no_repeats(T;[u / v])
6. no_repeats(T;bs)
7. [u / v] ⊆ bs
⊢ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ ds)
BY
{ ((Assert (u ∈ bs) BY
          (RepeatFor 2 (UnfoldTopAb (-1)) THEN InstHyp [⌜0⌝] (-1)⋅ THEN Auto))⋅
   THEN (FLemma `l_member_decomp` [-1] THENA Auto)
   ) }

1
1. [T] : Type
2. u : T
3. v : T List
4. bs : T List
5. no_repeats(T;[u / v])
6. no_repeats(T;bs)
7. [u / v] ⊆ bs
8. (u ∈ bs)
9. ∃l1,l2:T List. (bs = (l1 @ [u] @ l2) ∈ (T List))
⊢ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ ds)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  bs  :  T  List
5.  no\_repeats(T;[u  /  v])
6.  no\_repeats(T;bs)
7.  [u  /  v]  \msubseteq{}  bs
\mvdash{}  \mexists{}cs,ds:T  List.  ((bs  =  (cs  @  [u  /  ds]))  \mwedge{}  v  \msubseteq{}  cs  @  ds)


By

---

Latex:
((Assert  (u  \mmember{}  bs)  BY
                (RepeatFor  2  (UnfoldTopAb  (-1))  THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))\mcdot{}
  THEN  (FLemma  `l\_member\_decomp`  [-1]  THENA  Auto)
  )

---

Home Index