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