Step * of Lemma strong-subtype-bag

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

1
.....subterm..... T:t
1:n
1. Type
2. Type
3. strong-subtype(A;B)
4. bag(A) ⊆bag(B)
5. {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