∀ (α : Type u_1) [inst : Inhabited α] [inst_1 : DecidableEq α] (x : Option { a // a ≠ default }),
  (if h : Option.elim' default Subtype.val x = default then none else some ⟨Option.elim' default Subtype.val x, h⟩) = x