(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
in
PET.mk_tactic assumption_tac
in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
in
PET.mk_tactic assumption_tac