---

Step * of Lemma l_contains-no_repeats-length

∀[T:Type]. ∀[as,bs:T List].  (||as|| ≤ ||bs||) supposing (as ⊆ bs and no_repeats(T;as))
BY
{ (Auto
   THEN RepUR ``l_contains l_all l_member`` -1
   THEN (Skolemize (-1) `f'  THENA Auto)
   THEN (BLemma `injection_le` THENA Auto)
   THEN With ⌜f⌝ (D 0)⋅
   THEN Auto'
   THEN Try ((ExtWith [`i'] [⌜i@0:ℕ||as|| ⟶ ℕ⌝]⋅ THEN Auto'))) }

1
1. T : Type
2. as : T List
3. bs : T List
4. no_repeats(T;as)
5. ∀i@0:ℕ||as||. ∃i:ℕ. (i < ||bs|| c∧ (as[i@0] = bs[i] ∈ T))
6. f : i@0:ℕ||as|| ⟶ ℕ
7. ∀i@0:ℕ||as||. (f i@0 < ||bs|| c∧ (as[i@0] = bs[f i@0] ∈ T))
⊢ Inj(ℕ||as||;ℕ||bs||;f)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (||as||  \mleq{}  ||bs||)  supposing  (as  \msubseteq{}  bs  and  no\_repeats(T;as))


By

---

Latex:
(Auto
  THEN  RepUR  ``l\_contains  l\_all  l\_member``  -1
  THEN  (Skolemize  (-1)  `f'    THENA  Auto)
  THEN  (BLemma  `injection\_le`  THENA  Auto)
  THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto'
  THEN  Try  ((ExtWith  [`i']  [\mkleeneopen{}i@0:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}]\mcdot{}  THEN  Auto')))

---

Home Index