---

Step * of Lemma bag-only_wf

∀[T:Type]. ∀[bs:bag(T)].  only(bs) ∈ T supposing #(bs) = 1 ∈ ℤ
BY
{ (Auto
   THEN newQuotD 2
   THEN Auto
   THEN Unfold `bag-size` -1
   THEN Unfold `bag-only` 0
   THEN FLemma `permutation-length` [-2]
   THEN Auto) }

1
1. T : Type
2. T List ∈ Type
3. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
4. ∀as:T List. permutation(T;as;as)
5. a : Base
6. b : Base
7. c : a = b ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
8. a ∈ T List
9. b ∈ T List
10. permutation(T;a;b)
11. ||a|| = 1 ∈ ℤ
12. ||a|| = ||b|| ∈ ℤ
⊢ hd(a) = hd(b) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    only(bs)  \mmember{}  T  supposing  \#(bs)  =  1


By

---

Latex:
(Auto
  THEN  newQuotD  2
  THEN  Auto
  THEN  Unfold  `bag-size`  -1
  THEN  Unfold  `bag-only`  0
  THEN  FLemma  `permutation-length`  [-2]
  THEN  Auto)

---

Home Index