---

Step * 1 of Lemma assert-bag-deq-member


1. A : Type
2. eq : EqDecider(A)
3. b : Base
4. b1 : Base
5. b = b1 ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. b ∈ A List
7. b1 ∈ A List
8. permutation(A;b;b1)
9. x : A
10. x1 : ↑x ∈b b
⊢ ∃L:A List. ((L = b ∈ bag(A)) ∧ (x ∈ L))
BY
{ (RW assert_pushdownC (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  b  :  Base
4.  b1  :  Base
5.  b  =  b1
6.  b  \mmember{}  A  List
7.  b1  \mmember{}  A  List
8.  permutation(A;b;b1)
9.  x  :  A
10.  x1  :  \muparrow{}x  \mmember{}\msubb{}  b
\mvdash{}  \mexists{}L:A  List.  ((L  =  b)  \mwedge{}  (x  \mmember{}  L))


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)\mcdot{}

---

Home Index