///|
#external
type HTMLVideoElement