simp [getUnique]
case intro
α : Type u_1
v x : α
⊢ getUnique {x} ⋯ = v ↔ {x} = {v}
case intro
α : Type u_1
v x : α
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v