---

Step * 1 of Lemma subtype_rel_unordered-combination


1. A : Type
2. B : Type
3. n : ℕ
4. strong-subtype(A;B)
5. x : bag(A)
6. bag-no-repeats(A;x)
7. #(x) = n ∈ ℤ
⊢ bag-no-repeats(B;x)
BY
{ (Thin (-1) THEN RepeatFor 3 (ParallelLast)) }

1
1. A : Type
2. B : Type
3. n : ℕ
4. strong-subtype(A;B)
5. x : bag(A)
6. L : A List
7. (L = x ∈ bag(A)) ∧ no_repeats(A;L)
⊢ (L = x ∈ bag(B)) ∧ no_repeats(B;L)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  n  :  \mBbbN{}
4.  strong-subtype(A;B)
5.  x  :  bag(A)
6.  bag-no-repeats(A;x)
7.  \#(x)  =  n
\mvdash{}  bag-no-repeats(B;x)


By

---

Latex:
(Thin  (-1)  THEN  RepeatFor  3  (ParallelLast))

---

Home Index