Tacticals.then_
~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
~continuation:(Tacticals.then_
~start:(VariousTactics.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
Tacticals.then_
~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
~continuation:(Tacticals.then_
~start:(VariousTactics.elim_type_tac ~term:_False)
~continuation:(assumption_tac))