Let x be given.

Assume HxnotK: ¬ (x ∈ K_set).

Assume Hx1: x = 1.

We will prove False.

Apply HxnotK to the current goal.

rewrite the current goal using Hx1 (from left to right).

An exact proof term for the current goal is one_in_K_set.

∎