- dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
-val destruct : term:Cic.term -> ProofEngineTypes.tactic
+ dbd:HSql.dbd ->
+ params:Auto.auto_params ->
+ universe:Universe.universe -> ProofEngineTypes.tactic
+val destruct : Cic.term list option -> ProofEngineTypes.tactic