• David Swasey's avatar
    Add `wp_stuckness_mono`. · 8307c4c3
    David Swasey authored
    This is derived from `wp_forget_not_stuck` and a trivial preorder on
    stuckness bits. (The two lemmas are redundant, but I have examples
    where each seems more natural than the other.)
    
    I did *not* bake `wp_stuckness_mono` into `strong_mono` for two
    reasons. Mainly, I didn't see a nice way to combine the two proofs
    (beyond `cut`). Less important, changing the type of `wp_strong_mono`
    will break code.
    8307c4c3
language.v 5.99 KB