---

Step * 1 of Lemma no_repeats-length-le-by-relation


1. A : Type
2. B : Type
3. R : A ⟶ B ⟶ ℙ
4. ∀a1,a2:A. ∀b:B.  ((R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A))
5. as : A List
6. bs : B List
7. no_repeats(A;as)
8. ∀i@0:ℕ||as||. ∃i:ℕ||bs||. (R as[i@0] bs[i])
9. f : i@0:ℕ||as|| ⟶ ℕ||bs||
10. ∀i@0:ℕ||as||. (R as[i@0] bs[f i@0])
11. a1 : ℕ||as||
12. a2 : ℕ||as||
13. (f a1) = (f a2) ∈ ℕ||bs||
14. as[a1] = as[a2] ∈ A
⊢ a1 = a2 ∈ ℕ||as||
BY
{ (SupposeNot THEN (D 7 With ⌜a1⌝  THENA Auto) THEN InstHyp [⌜a2⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  R  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}a1,a2:A.  \mforall{}b:B.    ((R  a1  b)  {}\mRightarrow{}  (R  a2  b)  {}\mRightarrow{}  (a1  =  a2))
5.  as  :  A  List
6.  bs  :  B  List
7.  no\_repeats(A;as)
8.  \mforall{}i@0:\mBbbN{}||as||.  \mexists{}i:\mBbbN{}||bs||.  (R  as[i@0]  bs[i])
9.  f  :  i@0:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||bs||
10.  \mforall{}i@0:\mBbbN{}||as||.  (R  as[i@0]  bs[f  i@0])
11.  a1  :  \mBbbN{}||as||
12.  a2  :  \mBbbN{}||as||
13.  (f  a1)  =  (f  a2)
14.  as[a1]  =  as[a2]
\mvdash{}  a1  =  a2


By

---

Latex:
(SupposeNot  THEN  (D  7  With  \mkleeneopen{}a1\mkleeneclose{}    THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}a2\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index