+ dbd:HSql.dbd ->
+ params:Auto.auto_params ->
+ automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic
+val cases_intros :
+ ?howmany:int ->
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?pattern:ProofEngineTypes.lazy_pattern ->
+ Cic.term -> ProofEngineTypes.tactic