theorem String.hash_eq {s : String} : hash s = s.hash

theorem String.Slice.hash_eq {s : Slice} : hash s = s.copy.hash

instance String.Slice.instLawfulHashable : LawfulHashable Slice