Results from experiments...
Result for decodeK
FAILURE
Result for codeK
FAILURE
Result for ltn_code
FAILURE
Result for gtn_decode
FAILURE
Result for seq_of_optK
FAILURE
Result for tag_of_pairK
FAILURE
Result for pair_of_tagK
FAILURE
Result for opair_of_sumK
FAILURE
Result for bool_of_unitK
FAILURE
Result for codeK
FAILURE
Result for correct
FAILURE
Result for complete
FAILURE
Result for extensional
FAILURE
Result for xchooseP
FAILURE
Result for eq_xchoose
FAILURE
Result for sigW
FAILURE
Result for sig2W
FAILURE
Result for sig_eqW
FAILURE
Result for sig2_eqW
FAILURE
Result for chooseP
FAILURE
Result for choose_id
FAILURE
Result for eq_choose
FAILURE
Result for PcanChoiceMixin
FAILURE
Result for pickleK
FAILURE
Result for pickle_invK
FAILURE
Result for pickleK_inv
FAILURE
Result for pcan_pickleK
FAILURE
Result for pickle_seqK
FAILURE
Result for pickle_taggedK
FAILURE
Result for nat_pickleK
SUCCESS
There were 1 out of 30 proven by Coq auto tactics
On average, a proof was found automatically after 2093 milliseconds
On average, a proof attempt took 1471 milliseconds