---

Step * 1 2 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. Inj(ℕ||L1||;ℕ||filter(λy.(¬b(= y x));L2)||;f)
16. ||L1|| ≤ ||filter(λy.(¬b(= y x));L2)||
⊢ (∃x@0∈L2. ¬¬(x@0 = x ∈ T))
BY
{ (BLemma `l_exists_iff`  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.  Inj(\mBbbN{}||L1||;\mBbbN{}||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||;f)
16.  ||L1||  \mleq{}  ||filter(\mlambda{}y.(\mneg{}\msubb{}(=  y  x));L2)||
\mvdash{}  (\mexists{}x@0\mmember{}L2.  \mneg{}\mneg{}(x@0  =  x))


By

---

Latex:
(BLemma  `l\_exists\_iff`    THEN  Auto)

---

Home Index