---

Step * 1 1 1 1 1 of Lemma permutation-when-no_repeats


1. T : Type
2. sa : T List
3. sb : T List
4. ∀x:T. ((x ∈ sa) ⇐⇒ (x ∈ sb))
5. no_repeats(T;sb)
6. no_repeats(T;sa)
7. ∀i:ℕ||sa||. ∃j:ℕ||sb||. (sa[i] = sb[j] ∈ T)
8. f : i:ℕ||sa|| ⟶ ℕ||sb||
9. ∀i:ℕ||sa||. (sa[i] = sb[f i] ∈ T)
10. a1 : ℕ||sa||
11. a2 : ℕ||sa||
12. (f a1) = (f a2) ∈ ℕ||sb||
13. ¬(a1 = a2 ∈ ℕ||sa||)
⊢ a1 = a2 ∈ ℕ||sa||
BY
{ OnMaybeHyp 6 (\h. (Unfold `no_repeats` h
                     THEN (InstHyp [⌜a1⌝;⌜a2⌝] h⋅ THEN Auto)
                     THEN (D -1 THEN RWO "-5" 0 THEN Auto)⋅)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  sa  :  T  List
3.  sb  :  T  List
4.  \mforall{}x:T.  ((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  sb))
5.  no\_repeats(T;sb)
6.  no\_repeats(T;sa)
7.  \mforall{}i:\mBbbN{}||sa||.  \mexists{}j:\mBbbN{}||sb||.  (sa[i]  =  sb[j])
8.  f  :  i:\mBbbN{}||sa||  {}\mrightarrow{}  \mBbbN{}||sb||
9.  \mforall{}i:\mBbbN{}||sa||.  (sa[i]  =  sb[f  i])
10.  a1  :  \mBbbN{}||sa||
11.  a2  :  \mBbbN{}||sa||
12.  (f  a1)  =  (f  a2)
13.  \mneg{}(a1  =  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
OnMaybeHyp  6  (\mbackslash{}h.  (Unfold  `no\_repeats`  h
                                      THEN  (InstHyp  [\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]  h\mcdot{}  THEN  Auto)
                                      THEN  (D  -1  THEN  RWO  "-5"  0  THEN  Auto)\mcdot{}))

---

Home Index