idris-0.12.3: test/unique004/unique001d.idr

steal : {a : UniqueType} -> Borrowed a -> a
steal (Read x) = x