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