---

Step * of Lemma set-equal-no_repeats-length

∀[T:Type]. ∀[as,bs:T List].
  (||as|| = ||bs|| ∈ ℤ) supposing (set-equal(T;as;bs) and no_repeats(T;bs) and no_repeats(T;as))
BY
{ (Auto
   THEN (Assert as ⊆ bs ∧ bs ⊆ as BY
               (InstLemma `set-equal-l_contains` [⌜T⌝;⌜as⌝;⌜bs⌝]⋅ THEN Auto))
   THEN D -1
   THEN RepeatFor 2 ((FLemma `l_contains-no_repeats-length` [-2] THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].
    (||as||  =  ||bs||)  supposing  (set-equal(T;as;bs)  and  no\_repeats(T;bs)  and  no\_repeats(T;as))


By

---

Latex:
(Auto
  THEN  (Assert  as  \msubseteq{}  bs  \mwedge{}  bs  \msubseteq{}  as  BY
                          (InstLemma  `set-equal-l\_contains`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  RepeatFor  2  ((FLemma  `l\_contains-no\_repeats-length`  [-2]  THENA  Auto))
  THEN  Auto)

---

Home Index