Proofs in Polyadic QL

Construct proofs for the following arguments:

1. (∃x)(Ax & ~(∃y)(By & Lxy)), (x)(Ex ⊃ Bx) // (∃x)(Ax & (y)(Ey  ⊃ ~Lxy))
2. (x)(y)((Hx & Oxy) ⊃ By), (x)(Bx ⊃ ~Sx) // (x)(y)((Hx & Oxy) ⊃ ~Sy)
3. (x)(y)(Rxy ⊃ ~Ryx) // (x)~Rxx
4. (x)~Rxx, (x)(y)(z)((Rxy & Ryz) ⊃ Rxz)  // (x)(y)(Rxy ⊃ ~Ryx)
5. (x)(y)(Fxy ≡ (Gx & ~Gy)), (∃x)(∃y)(Fxy & Fyx) // (∃x)(Gx & ~Gx)   
6. (x)(y)(Fxy ⊃ Gxy), (x)(y)(Gxy ⊃ Hxy) // (x)(y)(Fxy ⊃ Hxy)
7. (x)((Tx & Sx) ⊃ Lax),  (∃x)~(~Tx v ~Sx) // (∃x)Lax
8. (x)Lax, (∃x)(Lax & Lxb), (x)(y)(Lxy ⊃ Lyx) // Lba
9. (x)((Wx v Cx) ⊃ Eax) // (x)(Wx ⊃ Eax)

Prove the following theorems:

1. (x)(y)Bxy ⊃ (∃x)(∃y)Bxy
2. (∃x)(y)(z)Rxyz ⊃ (y)(z)(∃x)Rxyz
3. (∃x)(∃y)(∃z)((Axy &Ayz) ⊃ Axz)
4. (Lab & ~Lba) ⊃ ~(x)(y)(Lxy ⊃ Lyx)