idris-0.99.1: test/totality020/totality020.idr

%default total

bug : (n, m : Nat) -> n + m = n -> Void
bug _ _ Refl impossible