---

Step * 1 1 2 of Lemma append_functionality_wrt_permutation

.....eq aux..... 
1. A : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
⊢ ℕ||as1|| + ||as2|| ∈ Type
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  A  :  Type
2.  as1  :  A  List@i
3.  as2  :  A  List@i
4.  bs1  :  A  List@i
5.  bs2  :  A  List@i
6.  f1  :  \mBbbN{}||as1||  {}\mrightarrow{}  \mBbbN{}||as1||@i
7.  Inj(\mBbbN{}||as1||;\mBbbN{}||as1||;f1)
8.  bs1  =  (as1  o  f1)
9.  f  :  \mBbbN{}||as2||  {}\mrightarrow{}  \mBbbN{}||as2||@i
10.  Inj(\mBbbN{}||as2||;\mBbbN{}||as2||;f)
11.  bs2  =  (as2  o  f)
12.  ||as1||  =  ||bs1||
13.  ||as2||  =  ||bs2||
\mvdash{}  \mBbbN{}||as1||  +  ||as2||  \mmember{}  Type


By

---

Latex:
TACTIC:Auto

---

Home Index