let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in