let lapply_tac (proof, goal) =
let xuri, metasenv, _subst, u, t, attrs = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lapply_tac (proof, goal) =
let xuri, metasenv, _subst, u, t, attrs = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in