let ty_term,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then ProofEngineTypes.apply_tactic
(P.apply_tac
~term:(
let ty_term,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then ProofEngineTypes.apply_tactic
(P.apply_tac
~term:(