---

Step * of Lemma strong-subtype-bag

∀[A,B:Type].  strong-subtype(bag(A);bag(B)) supposing strong-subtype(A;B)
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto)) THEN ExRepD) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. strong-subtype(A;B)
4. bag(A) ⊆r bag(B)
5. x : {b:bag(B)| ∃a:bag(A). (b = a ∈ bag(B))} 
⊢ x ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    strong-subtype(bag(A);bag(B))  supposing  strong-subtype(A;B)


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto))  THEN  ExRepD)

---

Home Index