---

Step * 1 of Lemma bag-append_wf

.....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)
BY
{ (BLemma `append_functionality_wrt_permutation` THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  as  :  Base
3.  a1  :  Base
4.  as  =  a1
5.  as  \mmember{}  T  List
6.  a1  \mmember{}  T  List
7.  permutation(T;as;a1)
8.  bs  :  Base
9.  b1  :  Base
10.  bs  =  b1
11.  bs  \mmember{}  T  List
12.  b1  \mmember{}  T  List
13.  permutation(T;bs;b1)
\mvdash{}  permutation(T;as  @  bs;a1  @  b1)


By

---

Latex:
(BLemma  `append\_functionality\_wrt\_permutation`  THEN  Auto)\mcdot{}

---

Home Index