Claim L0: ∀ x0 x1 x2 . (λ x3 x4 . False) x0 x1 ⟶ (λ x3 x4 . False) x0 x2 ⟶ x1 = x2

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: False.

Apply FalseE with (λ x3 x4 . False) x0 x2 ⟶ x1 = x2.

The subproof is completed by applying H0.

Claim L1: ∃ x0 . ∀ x1 . iff (prim1 x1 x0) (∃ x2 . and (prim1 x2 (prim0 (λ x3 . False))) False)

Apply unknownprop_aaea0f1d3f5e853f0d3287d822ec5f356e024921388ea00672dad551690ba08f with prim0 (λ x0 . False), λ x0 x1 . False.

The subproof is completed by applying L0.

Apply L1 with ∃ x0 . ∀ x1 . nIn x1 x0.

Let x0 of type ι be given.

Assume H2: ∀ x1 . iff (prim1 x1 x0) (∃ x2 . and (prim1 x2 (prim0 (λ x3 . False))) False).

Let x1 of type ο be given.

Assume H3: ∀ x2 . (∀ x3 . nIn x3 x2) ⟶ x1.

Apply H3 with x0.

Let x2 of type ι be given.

Assume H4: prim1 x2 x0.

Apply H2 with x2, False.

Assume H5: prim1 x2 x0 ⟶ ∃ x3 . and (prim1 x3 (prim0 (λ x4 . False))) False.

Assume H6: (∃ x3 . and (prim1 x3 (prim0 (λ x4 . False))) False) ⟶ prim1 x2 x0.

Apply H5 with False leaving 2 subgoals.

The subproof is completed by applying H4.

Let x3 of type ι be given.

Assume H7: (λ x4 . and (prim1 x4 (prim0 (λ x5 . False))) False) x3.

Apply H7 with False.

Assume H8: prim1 x3 (prim0 (λ x4 . False)).

Assume H9: False.

The subproof is completed by applying H9.

■

Proofgold Proof