let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactics = HEL.list_rev_map_filter map context in
let result = PET.apply_tactic (T.seq ~tactics) status in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactics = HEL.list_rev_map_filter map context in
let result = PET.apply_tactic (T.seq ~tactics) status in