let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
match auto_main tables newmeta context flags [elem] universe cache with
| Success (metasenv,subst,_), tables,cache,_ ->
let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
match auto_main tables newmeta context flags [elem] universe cache with
| Success (metasenv,subst,_), tables,cache,_ ->