An exact proof term for the current goal is (set_ext 1 (Sing 0) Subq_1_Sing0 Subq_Sing0_1).