GenericMonkey

Edited to simplify the min repro, as I realized the extra `lemma` wasn't necessary. Original, for reference: ```dafny ghost predicate trigger1(x : nat) { true } lemma Test1() ensures exists...

Latest commit moves some things around to allow for ported `ne` proofs to be instances of `NonExpansive₂`. However, there is some potential clunkiness here, as `ContractiveABA` and `ContractiveABB` had to...

Eliminated `ContractiveABA` and `ContractiveABB` completely, all results now use `(fA : α -c> β -n> α)` and `(fB : α -c> β -c> β)` instead. If this is undesirable (in...

Sorry for the delay -- had stepped out for the holidays. Your changes look good, I'm good to merge. Thanks for your help 😀