let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)