[Agda] What is wrong about this proof for A ⊆ A ∪ B

[Katsutoshi Itoh]

Hi all.

I'm studying sets theory by using agda(2.5.1).
Now, I've proved a theorem A ⊆ A ∪ B by 2 kind of solutions,
and I get warnings(yellow highlight) occured around both codes,
But I couldn't understand what's happen.
Please teach me what is wrong about these?

```
  A⊆A∪B : ∀ A B → A ⊆ A ∪ B
  A⊆A∪B x∈A B x = inj₁ x

  A⊆A∪B' : ∀ {ℓ₀ ℓ₁ X} {A : Pred X ℓ₀} {B : Pred X ℓ₁} → A ⊆ A ∪ B
  A⊆A∪B' x∈A = inj₁ x∈A
```

I attach all my program file.

Regards.

-- 
----
いとう かつとし
cutsea110 at gmail.com
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.agda
Type: application/octet-stream
Size: 7163 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20160615/7e5d5415/test.obj