Ki Yung Ahn

For local declarations, overlapping patterns warning works well. For global or module level definitions, however, I cannot find a way to enable warnings for overlapping patterns. `:set -Wall` only complains...

I've copied and pasted the exactly the same lemma whose argument is a disjunction of object logic propositions. When trying to prove it by itself Abella complains that unification fails...