looking for constructors. If the two sides differ on two constructors,
it closes the current goal. If they differ by other two terms it introduces
an equality. *)
-val destruct_tac: Cic.term option -> ProofEngineTypes.tactic
+val destruct_tac: Cic.term list option -> ProofEngineTypes.tactic