---

Step * 1 of Lemma list-diff2-sym


1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. b : T
5. c : T
⊢ as-[b; c] = as-[c; b] ∈ (T List)
BY
{ (BLemma `list-diff_functionality`
   THEN Auto
   THEN RepeatFor 2 ((RW  ListC (-1) THENA Auto))
   THEN RepeatFor 2 ((RW  ListC 0 THENA Auto))
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  as  :  T  List
4.  b  :  T
5.  c  :  T
\mvdash{}  as-[b;  c]  =  as-[c;  b]


By

---

Latex:
(BLemma  `list-diff\_functionality`
  THEN  Auto
  THEN  RepeatFor  2  ((RW    ListC  (-1)  THENA  Auto))
  THEN  RepeatFor  2  ((RW    ListC  0  THENA  Auto))
  THEN  D  -1
  THEN  Auto)

---

Home Index