Let X be given.

Assume H1: X ∈ 𝒫 0.

We will prove X ∈ {0}.

We prove the intermediate claim L1: X = 0.

Apply Empty_Subq_eq to the current goal.

An exact proof term for the current goal is (PowerE 0 X H1).

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

We will prove 0 ∈ {0}.

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

Let X be given.

Assume H1: X ∈ {0}.

We will prove X ∈ 𝒫 0.

rewrite the current goal using (SingE 0 X H1) (from left to right).

We will prove 0 ∈ 𝒫 0.

An exact proof term for the current goal is (Empty_In_Power 0).