More efficient conversion of pmap to association lists.
Prove better correspondence between Permutation and contains.
Make arguments of proj1_sig maximally implicit.
More properties about the rationals Qc.
Two basic De Morgan like laws for decidable propositions.
Use wf_projected instead of well_founded_lt_compat