---

Step * 1 of Lemma remove-repeats_functionality_wrt_permutation


1. [T] : Type
2. eq : EqDecider(T)
3. n : ℕ
4. ∀L2:T List
     (||L2|| < ||[]||
     ⇒ (∀L3:T List. (permutation(T;L2;L3) ⇒ permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
5. L2 : T List
6. permutation(T;[];L2)
⊢ permutation(T;remove-repeats(eq;[]);remove-repeats(eq;L2))
BY
{ ((FLemma `permutation-nil-iff` [-1] THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN BLemma `permutation-nil`
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  n  :  \mBbbN{}
4.  \mforall{}L2:T  List
          (||L2||  <  ||[]||
          {}\mRightarrow{}  (\mforall{}L3:T  List
                      (permutation(T;L2;L3)  {}\mRightarrow{}  permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
5.  L2  :  T  List
6.  permutation(T;[];L2)
\mvdash{}  permutation(T;remove-repeats(eq;[]);remove-repeats(eq;L2))


By

---

Latex:
((FLemma  `permutation-nil-iff`  [-1]  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  BLemma  `permutation-nil`
  THEN  Auto)\mcdot{}

---

Home Index