---

Step * of Lemma bag-member-implies-hd-append

∀[T:Type]. ∀[x:T]. ∀[b:bag(T)].  ↓∃c:bag(T). (b = ({x} + c) ∈ bag(T)) supposing x ↓∈ b
BY
{ (Auto
   THEN (BagToList (-2) THENA Auto)
   THEN D (-1)
   THEN ExRepD
   THEN (RevHypSubst' (-2) 0 THENA Auto)
   THEN ThinVar `b'
   THEN ThinTrivial
   THEN RepeatFor 2 (D (-1))
   THEN D 0
   THEN (InstConcl [⌜L\[i]⌝]⋅ THENA Auto)
   THEN RepUR ``single-bag bag-append`` 0
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN ThinVar `x'
   THEN EqTypeCD
   THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. L : T List
3. i : ℕ
4. i < ||L||
⊢ permutation(T;L;[L[i] / L\[i]])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    \mdownarrow{}\mexists{}c:bag(T).  (b  =  (\{x\}  +  c))  supposing  x  \mdownarrow{}\mmember{}  b


By

---

Latex:
(Auto
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  D  (-1)
  THEN  ExRepD
  THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  ThinTrivial
  THEN  RepeatFor  2  (D  (-1))
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}L\mbackslash{}[i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``single-bag  bag-append``  0
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  ThinVar  `x'
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index