totality026.idr

import Data.Vect

total
p : Elem (Maybe x) (map Maybe xs) -> Elem x xs
p Here impossible
p (There l) impossible