Skip to content

Better way of writing `Proper` premises in fin sets

Robbert Krebbers requested to merge robbert/better_proper into master

Use Proper (.. => impl) instead of Proper (.. => iff) and ∀ x, Proper .. instead of Proper ((=) ==> ..).

The new premises are easier to prove (both solve_proper and manual proof).

This came up in !478 (merged)

Merge request reports