---

Step * 1 2 1 1 1 2 1 of Lemma fset-size-remove


∀T:Type. ∀eq:EqDecider(T). ∀x:T. ∀L:T List.
  ((no_repeats(T;L) ∧ (x ∈ L)) ⇒ (filter(λx@0.(¬b(eq x@0 x));L) = remove-first(λy.(eq y x);L) ∈ (T List)))
BY
{ TACTIC:(Unfold `remove-first` 0 THEN InductionOnList THEN (Reduce 0 THEN Auto) THEN AutoBoolCase ⌜eq u x⌝⋅) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : T@i
4. u : T@i
5. v : T List@i
6. (no_repeats(T;v) ∧ (x ∈ v))
⇒ (filter(λx@0.(¬b(eq x@0 x));v)
   = rec-case(v) of
     [] => []
     a::as =>
      r.if (λy.(eq y x)) a then as else [a / r] fi 
   ∈ (T List))
7. no_repeats(T;[u / v])
8. (x ∈ [u / v])
9. u = x ∈ T
⊢ filter(λx@0.(¬b(eq x@0 x));v) = v ∈ (T List)

2
1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : T@i
4. u : T@i
5. ¬(u = x ∈ T)
6. v : T List@i
7. (no_repeats(T;v) ∧ (x ∈ v))
⇒ (filter(λx@0.(¬b(eq x@0 x));v)
   = rec-case(v) of
     [] => []
     a::as =>
      r.if (λy.(eq y x)) a then as else [a / r] fi 
   ∈ (T List))
8. no_repeats(T;[u / v])
9. (x ∈ [u / v])
⊢ [u / filter(λx@0.(¬b(eq x@0 x));v)]
= [u / rec-case(v) of [] => [] | h::t => r.if eq h x then t else [h / r] fi ]
∈ (T List)

---

Latex:

---

Latex:

\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:T  List.
    ((no\_repeats(T;L)  \mwedge{}  (x  \mmember{}  L))  {}\mRightarrow{}  (filter(\mlambda{}x@0.(\mneg{}\msubb{}(eq  x@0  x));L)  =  remove-first(\mlambda{}y.(eq  y  x);L)))


By

---

Latex:
TACTIC:(Unfold  `remove-first`  0
                THEN  InductionOnList
                THEN  (Reduce  0  THEN  Auto)
                THEN  AutoBoolCase  \mkleeneopen{}eq  u  x\mkleeneclose{}\mcdot{})

---

Home Index