Assume H1: TransSet {1}.

We prove the intermediate claim L1: 0 ∈ {1}.

An exact proof term for the current goal is H1 1 (SingI 1) 0 In_0_1.

Apply neq_0_1 to the current goal.

An exact proof term for the current goal is SingE 1 0 L1.

∎