---

Step * 1 1 of Lemma respects-equality-bag


1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
⊢ (bs ∈ B List) ∧ permutation(B;as;bs)
BY
{ ((Assert as = (bs o f) ∈ (B List) BY
          (ChangeEquality ⌜A List⌝⋅ THEN Auto))
   THEN (Assert permutation(B;bs;as) BY
               (D 0 With ⌜f⌝  THEN Auto))
   THEN (Assert ⌜bs ∈ B List⌝⋅ THENM Auto)) }

1
.....assertion..... 
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
11. as = (bs o f) ∈ (B List)
12. permutation(B;bs;as)
⊢ bs ∈ B List

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  respects-equality(A;B)
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
7.  as  \mmember{}  B  List
8.  f  :  \mBbbN{}||bs||  {}\mrightarrow{}  \mBbbN{}||bs||
9.  Inj(\mBbbN{}||bs||;\mBbbN{}||bs||;f)
10.  as  =  (bs  o  f)
\mvdash{}  (bs  \mmember{}  B  List)  \mwedge{}  permutation(B;as;bs)


By

---

Latex:
((Assert  as  =  (bs  o  f)  BY
                (ChangeEquality  \mkleeneopen{}A  List\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  permutation(B;bs;as)  BY
                          (D  0  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto))
  THEN  (Assert  \mkleeneopen{}bs  \mmember{}  B  List\mkleeneclose{}\mcdot{}  THENM  Auto))

---

Home Index