---

Step * of Lemma bag-append_wf

∀[T:Type]. ∀[as,bs:bag(T)].  (as + bs ∈ bag(T))
BY
{ ((UnivCD THENA Auto)
   THEN (DVar `as' THEN Auto THEN DVar `bs' THEN Auto THEN Unfold `bag-append` 0 THEN EqTypeCD THEN Auto)⋅
   ) }

1
.....antecedent..... 
1. T : Type
2. as : Base
3. a1 : Base
4. as = a1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
5. as ∈ T List
6. a1 ∈ T List
7. permutation(T;as;a1)
8. bs : Base
9. b1 : Base
10. bs = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
11. bs ∈ T List
12. b1 ∈ T List
13. permutation(T;bs;b1)
⊢ permutation(T;as @ bs;a1 @ b1)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].    (as  +  bs  \mmember{}  bag(T))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (DVar  `as'
              THEN  Auto
              THEN  DVar  `bs'
              THEN  Auto
              THEN  Unfold  `bag-append`  0
              THEN  EqTypeCD
              THEN  Auto)\mcdot{}
  )

---

Home Index