theorem elArrayList (A: set) (l n: nat): $ l e. Array A n -> l e. List A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elArray | l e. Array A n <-> l e. List A /\ len l = n |
|
2 | anl | l e. List A /\ len l = n -> l e. List A |
|
3 | 1, 2 | sylbi | l e. Array A n -> l e. List A |