_ /\ _ = E

mustBeType :: TT Relevance -> Ver ()
mustBeType ty = conv ty (V typeOfTypes)

verify :: Program Relevance -> Either VerFailure ()
verify prog = runVer (builtins relOfType) $ verProg prog

verProg :: Program Relevance -> Ver ()
verProg prog = do
    _ <- verTm R prog
    return ()

verDefs :: [Def Relevance] -> Ver ()
verDefs [] = return ()