---

Step * 2 2 of Lemma sublist-if-no_repeats


1. [A] : Type
2. R : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀bs:A List
     (StAntiSym(A;x,y.↑R[x;y])
     ⇒ Irrefl(A;x,y.↑R[x;y])
     ⇒ Trans(A;x,y.↑R[x;y])
     ⇒ no_repeats(A;v)
     ⇒ l-ordered(A;x,y.↑R[x;y];v)
     ⇒ l-ordered(A;x,y.↑R[x;y];bs)
     ⇒ (∀a:A. ((a ∈ v) ⇒ (a ∈ bs)))
     ⇒ v ⊆ bs)
6. bs : A List
7. StAntiSym(A;x,y.↑R[x;y])
8. Irrefl(A;x,y.↑R[x;y])
9. Trans(A;x,y.↑R[x;y])
10. no_repeats(A;v)
11. ¬(u ∈ v)
12. l-ordered(A;x,y.↑R[x;y];v)
13. ∀y:A. ((y ∈ v) ⇒ (↑R[u;y]))
14. l-ordered(A;x,y.↑R[x;y];bs)
15. (u ∈ bs)
16. ∀a:A. ((a ∈ v) ⇒ (a ∈ filter(λy.R[y;u];bs) @ [u / filter(λy.R[u;y];bs)]))
17. bs = (filter(λy.R[y;u];bs) @ [u / filter(λy.R[u;y];bs)]) ∈ (A List)
18. u = u ∈ A
19. a : A
20. (a ∈ v)
21. (a ∈ [u / filter(λy.R[u;y];bs)])
⊢ (a ∈ filter(λy.R[u;y];bs))
BY
{ ((RW ListC (-1) THENA Auto) THEN D (-1) THEN Auto THEN Assert ⌜False⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \mforall{}bs:A  List
          (StAntiSym(A;x,y.\muparrow{}R[x;y])
          {}\mRightarrow{}  Irrefl(A;x,y.\muparrow{}R[x;y])
          {}\mRightarrow{}  Trans(A;x,y.\muparrow{}R[x;y])
          {}\mRightarrow{}  no\_repeats(A;v)
          {}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];v)
          {}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];bs)
          {}\mRightarrow{}  (\mforall{}a:A.  ((a  \mmember{}  v)  {}\mRightarrow{}  (a  \mmember{}  bs)))
          {}\mRightarrow{}  v  \msubseteq{}  bs)
6.  bs  :  A  List
7.  StAntiSym(A;x,y.\muparrow{}R[x;y])
8.  Irrefl(A;x,y.\muparrow{}R[x;y])
9.  Trans(A;x,y.\muparrow{}R[x;y])
10.  no\_repeats(A;v)
11.  \mneg{}(u  \mmember{}  v)
12.  l-ordered(A;x,y.\muparrow{}R[x;y];v)
13.  \mforall{}y:A.  ((y  \mmember{}  v)  {}\mRightarrow{}  (\muparrow{}R[u;y]))
14.  l-ordered(A;x,y.\muparrow{}R[x;y];bs)
15.  (u  \mmember{}  bs)
16.  \mforall{}a:A.  ((a  \mmember{}  v)  {}\mRightarrow{}  (a  \mmember{}  filter(\mlambda{}y.R[y;u];bs)  @  [u  /  filter(\mlambda{}y.R[u;y];bs)]))
17.  bs  =  (filter(\mlambda{}y.R[y;u];bs)  @  [u  /  filter(\mlambda{}y.R[u;y];bs)])
18.  u  =  u
19.  a  :  A
20.  (a  \mmember{}  v)
21.  (a  \mmember{}  [u  /  filter(\mlambda{}y.R[u;y];bs)])
\mvdash{}  (a  \mmember{}  filter(\mlambda{}y.R[u;y];bs))


By

---

Latex:
((RW  ListC  (-1)  THENA  Auto)  THEN  D  (-1)  THEN  Auto  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index