let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let signature = MetadataQuery.signature_of metasenv goal in
let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let signature = MetadataQuery.signature_of metasenv goal in