allow arbitrary proof styles below cases
renaming
correctness fix: do not ignore failing cases
tuned
proof by extensionality
tuned