---

Step * 1 1 of Lemma length-eq-lists-diff-elts


1. T : Type
2. eq : ∀x,y:T.  Dec(x = y ∈ T)@i
3. L1 : T List@i
4. L2 : T List@i
5. no_repeats(T;L1)@i
6. ||L1|| ≥ ||L2|| @i
7. x : T@i
8. (x ∈ L2)@i
9. ¬(x ∈ L1)@i
10. ∀x:T. ((x ∈ L1) ⇒ (¬¬(x ∈ L2)))
11. = : EqDecider(T)
12. ∀i:ℕ||L1||. ∃j:ℕ||filter(λy.(¬b(= y x));L2)||. (L1[i] = filter(λy.(¬b(= y x));L2)[j] ∈ T)
13. f : i:ℕ||L1|| ─→ ℕ||filter(λy.(¬b(= y x));L2)||
14. ∀i:ℕ||L1||. (L1[i] = filter(λy.(¬b(= y x));L2)[f i] ∈ T)
15. a1 : ℕ||L1||@i
16. a2 : ℕ||L1||@i
17. (f a1) = (f a2) ∈ ℕ||filter(λy.(¬b(= y x));L2)||@i
⊢ a1 = a2 ∈ ℕ||L1||
BY
{ (SupposeNot
   THEN (With ⌈a1⌉ (D 5)⋅ THENA Auto)
   THEN InstHyp [⌈a2⌉] (-1)⋅
   THEN Auto
   THEN (InstHyp [⌈a1⌉] 13⋅ THENA Auto)
   THEN (InstHyp [⌈a2⌉] 13⋅ THENA Auto)
   THEN D -3
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  L1  :  T  List@i
4.  L2  :  T  List@i
5.  no\_repeats(T;L1)@i
6.  ||L1||  \mgeq{}  ||L2||  @i
7.  x  :  T@i
8.  (x  \mmember{}  L2)@i
9.  \mneg{}(x  \mmember{}  L1)@i
10.  \mforall{}x:T.  ((x  \mmember{}  L1)  {}\mRightarrow{}  (\mneg{}\mneg{}(x  \mmember{}  L2)))
11.  =  :  EqDecider(T)
12.  \mforall{}i:\mBbbN{}||L1||.  \mexists{}j:\mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||.  (L1[i]  =  filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)[j])
13.  f  :  i:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||
14.  \mforall{}i:\mBbbN{}||L1||.  (L1[i]  =  filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)[f  i])
15.  a1  :  \mBbbN{}||L1||@i
16.  a2  :  \mBbbN{}||L1||@i
17.  (f  a1)  =  (f  a2)@i
\mvdash{}  a1  =  a2


By

---

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

---

Home Index