Results from experiments... Result for In_compat FAILURE Result for mem_spec FAILURE Result for isok_iff FAILURE Result for add_spec FAILURE Result for remove_spec FAILURE Result for singleton_ok SUCCESS Result for singleton_spec FAILURE Result for empty_ok SUCCESS Result for empty_spec FAILURE Result for is_empty_spec FAILURE Result for elements_spec1 SUCCESS Result for elements_spec2w SUCCESS Result for fold_spec SUCCESS Result for union_spec FAILURE Result for inter_spec FAILURE Result for diff_spec FAILURE Result for subset_spec FAILURE Result for equal_spec FAILURE Result for cardinal_spec SUCCESS Result for filter_spec' FAILURE Result for filter_spec FAILURE Result for for_all_spec FAILURE Result for exists_spec FAILURE Result for partition_spec1 FAILURE Result for partition_spec2 FAILURE Result for partition_ok1' FAILURE Result for partition_ok2' FAILURE There were 6 out of 27 proven by Coq auto tactics On average, a proof was found automatically after 618 milliseconds On average, a proof attempt took 737 milliseconds