We prove the intermediate
claim H1in:
1 ∈ {1}.
An
exact proof term for the current goal is
(SingI 1).
We prove the intermediate
claim Hsub:
1 ⊆ {1}.
An
exact proof term for the current goal is
(H 1 H1in).
We prove the intermediate
claim H0in1:
0 ∈ 1.
An
exact proof term for the current goal is
In_0_1.
We prove the intermediate
claim H0inSing1:
0 ∈ {1}.
An
exact proof term for the current goal is
(Hsub 0 H0in1).
We prove the intermediate
claim Heq:
0 = 1.
An
exact proof term for the current goal is
(SingE 1 0 H0inSing1).
An
exact proof term for the current goal is
(neq_0_1 Heq).