Step
*
of Lemma
bag-remove-trivial
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  bs - x = bs ∈ bag(T) supposing ¬x ↓∈ bs
BY
{ (Auto
   THEN RepUR ``bag-remove`` 0
   THEN RWO "bag-filter-trivial2" 0
   THEN Auto
   THEN AllPushDown
   THEN ParallelOp -3
   THEN Assert ⌜x = y ∈ T⌝⋅
   THEN Auto
   THEN Unfold `deq` 2
   THEN DVarSets
   THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    bs  -  x  =  bs  supposing  \mneg{}x  \mdownarrow{}\mmember{}  bs
By
Latex:
(Auto
  THEN  RepUR  ``bag-remove``  0
  THEN  RWO  "bag-filter-trivial2"  0
  THEN  Auto
  THEN  AllPushDown
  THEN  ParallelOp  -3
  THEN  Assert  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Unfold  `deq`  2
  THEN  DVarSets
  THEN  Auto)
Home
Index