---

Step * 1 1 1 1 1 of Lemma l_contains-cons

.....assertion..... 
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 : T List
10. l2 : T List
11. bs = (l1 @ [u / l2]) ∈ (T List)
12. bs = (l1 @ [u / l2]) ∈ (T List)
13. a : T
14. (a ∈ v)
⊢ (a ∈ bs)
BY
{ OnMaybeHyp 7 (\h. (Unfold `l_contains` h THEN (RWO "l_all_iff" h THENA Auto) THEN BHyp h  THEN Auto THEN Auto)) }

---

Latex:

---

Latex:
.....assertion..... 
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
8.  (u  \mmember{}  bs)
9.  l1  :  T  List
10.  l2  :  T  List
11.  bs  =  (l1  @  [u  /  l2])
12.  bs  =  (l1  @  [u  /  l2])
13.  a  :  T
14.  (a  \mmember{}  v)
\mvdash{}  (a  \mmember{}  bs)


By

---

Latex:
OnMaybeHyp  7  (\mbackslash{}h.  (Unfold  `l\_contains`  h
                                      THEN  (RWO  "l\_all\_iff"  h  THENA  Auto)
                                      THEN  BHyp  h 
                                      THEN  Auto
                                      THEN  Auto))

---

Home Index