---

Step * of Lemma l_contains-eq_set-no_repeats

∀[T:Type]. ∀[as,bs:T List]. ∀[eq:EqDecider(T)].
  (no_repeats(T;as)) supposing (l_eqset(T;as;bs) and no_repeats(T;bs) and (||as|| = ||bs|| ∈ ℤ))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `remove-repeats-length-no-repeats` [⌜T⌝; ⌜eq⌝; ⌜bs⌝]⋅ THENA Auto)
   THEN (InstLemma `remove-repeats-set-equal` [⌜T⌝; ⌜eq⌝; ⌜as⌝; ⌜bs⌝]⋅
         THENA (Auto THEN Unfold `set-equal` 0⋅ THEN Unfold `l_eqset` (-2) THEN Auto)
         )
   THEN HypSubst' (-2) (-1)
   THEN (RWO "-5<" (-1) THENA Auto)
   THEN (InstLemma `remove-repeats-length-no-repeats-iff` [⌜T⌝; ⌜eq⌝; ⌜as⌝]⋅ THENA Auto)
   THEN BHyp (-1) 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].  \mforall{}[eq:EqDecider(T)].
    (no\_repeats(T;as))  supposing  (l\_eqset(T;as;bs)  and  no\_repeats(T;bs)  and  (||as||  =  ||bs||))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `remove-repeats-length-no-repeats`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `remove-repeats-set-equal`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}as\mkleeneclose{};  \mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Unfold  `set-equal`  0\mcdot{}  THEN  Unfold  `l\_eqset`  (-2)  THEN  Auto)
              )
  THEN  HypSubst'  (-2)  (-1)
  THEN  (RWO  "-5<"  (-1)  THENA  Auto)
  THEN  (InstLemma  `remove-repeats-length-no-repeats-iff`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  (-1) 
  THEN  Auto)

---

Home Index