---

Step * 1 of Lemma bag-drop-head

.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
⊢ bag-remove1(eq;[x / bs];x) ~ inl bs
BY
{ (Unfold `bag-remove1` 0 THEN RecUnfold `bag_remove1_aux` 0 THEN Reduce 0 THEN AutoSplit)⋅ }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  bag(T)
4.  x  :  T
\mvdash{}  bag-remove1(eq;[x  /  bs];x)  \msim{}  inl  bs


By

---

Latex:
(Unfold  `bag-remove1`  0  THEN  RecUnfold  `bag\_remove1\_aux`  0  THEN  Reduce  0  THEN  AutoSplit)\mcdot{}

---

Home Index