(* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
in
ProofEngineTypes.mk_tactic contradiction_tac
(* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
in
ProofEngineTypes.mk_tactic contradiction_tac