Skip to content

countable.v: prove choose_proper

Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:choose_proper into master

Needs the misplaced Acc_rect_max.

Add missing properness lemma for choose.

Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.

Edited by Paolo G. Giarrusso

Merge request reports